Is there any practical algorithm / data-structure that can't be done with non-recursive Lambda Calculus augmented with foldl?

Question

In my search for a practical non-turing complete programming language, I've been paying attention to lambda-calculus with disallowed self-application - that is, x x forbidden. After taking that language and augmenting it with lists and the foldl and range operations, pretty much any algorithm I've tried so far is implementable. It is trivial to implement filter, reverse, head, tail, map, scanl, zip and many others - foldl replaces the need for recursion.

Can you think in any practical, important algorithm that would be undoable in that language?

It is no coincidence that all of them use self-application—the application of an expression to itself. It is through self-application that repetitive computation can be simulated in the lambda calculus. Indeed, the third of the previous three examples is famous because it can encode recursive function definitions.

From http://people.cis.ksu.edu/~schmidt/705s13/Lectures/ch6.pdf .

• user7043: Undoable, or unfeasible due to excessive slowdown?
• user7043: Have you tried anything hat usually requires binary trees and/or random access to implement efficiently, such as associative maps? It appears to me that virtually all operations in this category would become linear time instead of logarithmic or constant time. This in turn makes many algorithms quadratic time instead of n log n time. Edit: I'm assuming "list" means linked list, so how can length be O(1) without compiler magic introducing a special cased length field?
• user7043: Well, I'm pretty sure you can replace every interesting tree with a flat list of some kind, at the cost of exponential slowdown. This is one of the reasons for more sophisticated means of guaranteeing termination (such as structural recursion) AFAIK.
• daniel gratzer: And how do you verify that there isn't self application? f [f] should be legal. Taking an iso-recursive Y combinator and changing fold' and unfold' to \x -> cons x ()' and car` respectively should work.
• daniel gratzer: @Dokkat Yeah I think you're in trouble here, read that blog post I linked above. It has an application of the Y combinator without self application. It relies on type level recursion but you don't have types so that's a non-issue. Voting to close.

Answer 1

tl;dr (or I don't know what a Y combinator is)

This question is based on the assumption that the above defined language is not Turing-complete, it actually is Turing-complete and therefore the question is invalid - all algorithms can be expressed in the language defined above as is the meaning of Turing-completeness.

---

Ok. Well apparently this has to be explicitly written out.

Proof of turing completeness follows trivially from unbounded recursion which can be derived from a fixpoint combinator.

Note the traditional Y combinator

Y f = (\x -> f (x x)) (\x -> f (x x))

Define

cons = \a b f -> f a b
car = \x y -> x
cdr = \x y -> y
fst = \p -> p car
snd = \p -> p cdr

This is just the standard encoding of church pairs.

nil = \x -> x -- Or anything really
fold = \x -> cons x nil
unfold = \x -> fst x

Then

Y f = (\x -> f (unfold x x)) (fold (\x -> f (unfold x x)))

No self application, but this still correctly encodes the Y combinator. I previously wrote this out in Haskell. There fold and unfold require more interesting jiggery-pokery because of types, but since lambda calculus has none we can safely ignore it :)

We've just proven we have a Turing-complete language. Every algorithm is therefore exactly as efficient as can be encoded in a Lambda Calculus. This also invalidates the question's original premise that the language is Turing-incomplete.

• Robert Harvey: For those of us that are hopelessly dense, can you tell us how this relates to the original question?
• daniel gratzer: @RobertHarvey Whoops sorry, this shows that Lambda calculus without self application is still turing complete. Therefore it is exactly as expressive lambda calculus.
• MaiaVictor: Alright, points for you. On the meantime, Tromps suggested this even simpler proof my premise was false: Y' = (λx. λy. x y x) (λy. λx. y (x y x))