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

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 deﬁnitions.

• 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
Dec 27, 2013 at 12:36
• 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.
– user7043
Dec 27, 2013 at 12:42
• 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. Dec 27, 2013 at 15:26
• @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. Dec 27, 2013 at 16:11

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.

``````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.

• For those of us that are hopelessly dense, can you tell us how this relates to the original question? Dec 27, 2013 at 20:21
• @RobertHarvey Whoops sorry, this shows that Lambda calculus without self application is still turing complete. Therefore it is exactly as expressive lambda calculus. Dec 27, 2013 at 20:24
• 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))` Dec 27, 2013 at 21:01