<p>Inside <a href="https://github.com/Muzietto/es6-lambda-calculus">a lambda calculus implementation for ECMASCript 6</a>, we are trying to implement new constructs such as type tags for strong typing, and conditionals such as the <code>if</code> statement by wrapping in lambdas the branches of the conditional.</p>

<p>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 <code>while</code> loops, which are not available in the primitives of lambda calculus? Is there a related impossibility result?</p>

CC BY-SA 3.0
2016-03-31T21:56:19.020Z
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
CC BY-SA 3.0
2016-04-01T09:00:42.953Z
@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
<lambda-calculus>
Is it possible to implement tail recursion inside a lambda calculus built on top of functions?
giorgiosironi
# Is it possible to implement tail recursion inside a lambda calculus built on top of functions?

(Asked by: username_0 on 2016-03-30)

Inside [a lambda calculus implementation for ECMASCript 6](https://github.com/Muzietto/es6-lambda-calculus), 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?

**Tags:** lambda-calculus

> **Comments:**
> **username_1**: 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?  
> **username_2**: @username_1 - 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  

---

## 0 answers

