Is it possible to implement tail recursion inside a lambda calculus built on top of functions?

Inside a lambda calculus implementation for ECMASCript 6, we are trying to implement new constructs such as type tags for strong typing, and conditionals such as the if statement by wrapping in lambdas the branches of the conditional.

General recursion can also be implemented with the Y combinator. However, when trying to implement tail recursion we get an ever-expanding stack trace. Is it even possible to do so without resorting to while loops, which are not available in the primitives of lambda calculus? Is there a related impossibility result?

• I'm curious: the usual (Church) Y combinator does not have the property $Y\ f\rightarrow_\beta f\ (Y\ f)$. The Turing fixed-point combinator, defined as $\Theta=(\lambda x.\lambda y. y\ (x\ x\ y))\ (\lambda x.\lambda y. y\ (x\ x\ y))$ does, however. Do you still get stack explosion with this? – cody Mar 31 '16 at 21:56
• @cody - Please note that all this has to run in a browser. Let's make an example. A simple addition function that can be fed to Y is ADD' f x y = (ISZERO y) x (f f (SUCC x)(PRED y)). Doing Y(ADD') blows the stack and I was able to avoid this using laziness. In any case, a stack is built even though lazily. If I try THETA(ADD') I see there is no immediate blowup, but THETA(ADD')(ONE)(TWO) causes it due to the eager evaluation of both COND branches. I am struggling to see how to create a lazy ADD' to use with THETA. Please see the last commit in the repo mentioned in the question – Marco Faustinelli Apr 1 '16 at 9:00