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?

Computation occurs by applying functions. One way to keep applying functions forever is to have a function recursively apply itself. If we don’t use recursion, then we don’t literally have a notion of "itself" for a given function. But a function can apply a function given to it as argument. So this ever-running function should take a function, and apply it. Now, for execution to go on, that applied function should do the same: take a function as argument, and apply it. This reasoning leads us to the canonical non-terminating program that does not use any recursion construct:

{{fun {x} {x x}}
{fun {x} {x x}}}

Note: This term is so well-known that it has a name. It’s called omega, Ω.

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

We can apply the same idea of "passing around the function to call next" in order to define a recursive function like sum, without using rec. Recall that our attempt at defining a recursive function:

{with {sum {fun {n}
{if0 n 0 {+ n {sum {- n 1}}}}}}
{sum 10}}

fails because sum is not bound in the body of the fun. In other words, the function does not know (or does not have access to) the function it should call next, when it want to recurse. Fair enough, we can pass it as argument:

{with {sum {fun {sum}
             {fun {n}
               {if0 n 0 {+ n {sum {- n 1}}}}}}}
   {sum 10}}

Note how the whole function is now wrapped in a function that takes the next function to call as argument (I’m using the same name sum). Now, the above code is not well-typed: sum is a function that first takes a function, then a number, so applying it as {sum 10} is incorrect. We should first give it the function to call next, which is... sum itself! We have to use the same self application pattern in the body of the function:

{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}}

Note how both the recursive call inside the body of sum, and the outside call {sum 10} do not use self application anymore. The Y combinator does the job.

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:

{with {f {Y {fun {f}
{fun {x} body}}}}
...}

Exercise: Do it!

contents ← prev up next →

1	Expressiveness of the Lambda Calculus
2	Recursion: Efficiency Considerations

1.1	Non-terminating programs
1.2	Recursion without a recursion construct
1.3	The Y combinator