1 Expressiveness of the Lambda Calculus
Implementing rec using mutation in the interpreter puts in doubt the fact that the (pure) lambda calculus is expressive enough to be Turing complete, since this requires supporting recursive functions. This, however, is worrying because according to the Church-Turing thesis, Turing machines and lambda calculus are equally expressive.
1.1 Non-terminating programs
One of the defining characteristics of recursion is that it allows for infinite behavior, yielding the well-known Halting Problem. So the first question we can try to answer is: is it possible to define a program (without rec) that does not terminate?
{{fun {x} {x x}} {fun {x} {x x}}}
Evaluating Ω never stops, because reducing it yields exactly the same term: substitute {fun {x} {x x}} for x in the body {x x}, and you obtain... Ω. Note that the essence of the non-terminating behavior is the self application, {x x}.
Question: Can you give a type to {fun {x} {x x}}? What does it suggest regarding the expressiveness of the lambda calculus with simple types?
1.2 Recursion without a recursion construct
{with {sum {fun {n} {if0 n 0 {+ n {sum {- n 1}}}}}} {sum 10}}
{with {sum {fun {sum} {fun {n} {if0 n 0 {+ n {sum {- n 1}}}}}}} {sum 10}}
{with {sum {fun {sum} {fun {n} {if0 n 0 {+ n {{sum sum} {- n 1}}}}}}} {{sum sum} 10}}
This works! We can therefore define recursive functions without having to extend the language with a (mutation-based) rec construct. Ouff... Church and Turing were not mistaken.
1.3 The Y combinator
The solution above is a bit annoying to write programs, because one has to use self application explicitly. Fortunately, we can use the abstraction power (lambda!) of functional programming to extract the self application pattern and simplify both the definition and the use of recursive functions.
The result of this abstraction process is a higher-order function called the Y combinator, which takes as input a function (that itself expects a function to recurse, in addition to its standard arguments), and "closes the loop" by introducing self application. The produced function can be used as a normal function. Assuming that the Y combinator is in scope, the sum function can be defined and used as follows:
{with {sum {Y {fun {sum} {fun {n} {if0 n 0 {+ n {sum {- n 1}}}}}}}} {sum 10}}
How does Y look like? Here it is, in our language:
{fun {f} {with {h {fun {g} {fun {n} {{f {g g}} n}}}} {h h}}}
Note: To see how to derive the Y combinator step-by-step, look at The Why of Y. It’s not that hard, and it’s a very good exercise in λ-fu!
Consequently, we can treat rec as syntactic sugar, similarly to what we did for with. Assuming that Y is in scope (eg. it is in the initial environment used to run programs), the transformation consists in replacing:
{rec {f {fun {x} body}} ...}
{with {f {Y {fun {f} {fun {x} body}}}} ...}