In a purely functional language — like lambda calculus — programs are expressed as nested function calls. Repetition in such an environment requires that nesting of function calls continues until some condition is met. During the repetition, each function passes its result to the next function in the nested chain and this repetition is completed when a test for some condition passes. The repetitive behaviour I’ve just described is recursion:
Repetition in functional programming is based on recursion: the definition of something in terms of itself. The nested function call sequence which is to be repeated is given a name. If some condition is met within the sequence, then that name is invoked to repeat the nested function call sequence within itself. The condition often checks whether or not the end of a linear or nested object sequence has been reached.
Greg Michaelson — An Introduction to Functional Programming Through Lambda Calculus
A simple first pass at implementing recursion in lambda calculus is to
introduce additional syntax for defining a function with a name, and then
using that name within the function’s body. The following example defines
a function add that performs a mathematical addition of two numbers
using Church numerals
(which are not defined here).
def add x y =
if iszero y
then x
else add (succ x) (pred y)
This function adds two numbers by repeatedly taking one away from argument
y and adding it to argument x until there are no more y to take. An
interesting artifact of using recursion for this implementation is the
choice of when to evaluate a function’s arguments. For example, if we
choose to evaluate the add function by delaying evaluation of the
arguments, we encounter the following scenario.
add x y
if iszero y
then x
else add (succ x) (pred y)
$$ \Downarrow $$
add x y
if iszero y
then x
else ((
add x y
if iszero y
then x
else add (succ x) (pred y)))
$$ \Downarrow $$
add x y
if iszero y
then x
else ((
add x y
if iszero y
then x
else ((
add x y
if iszero y
then x
else add (succ x) (pred y)))
ad infinitum. In this example, I expanded the definition of add before
evaluating the arguments to add, and an infinite loop that will never
complete results.
Recursion and Fixed-Point Operators
The above example shows how lambda calculus does not directly support recursion using self-referential functions: we end up in an infinite loop. This is problematic because for lambda calculus to be useful requires that any program can be expressed using nested function calls — including functions that express looping using recursion. We can resolve this dilemma by using what is known as a fixed-point function.
In mathematics, a fixed point (sometimes shortened to fixpoint, also known as an invariant point) of a function is an element of the function’s domain that is mapped to itself by the function. That is to say, c is a fixed point of the function \(f(x)\) if \(f( c ) = c\). This means \(f(f(…f( c )…)) = f^n( c ) = c\), an important terminating consideration when recursively computing \(f\).
In other words, a fixed point of a function f is a value that does not change under the application of the function f. For example, the following function has two fixed-points — \(0\) and \(1\) — because \(f(0) = 0\) and \(f(1) = 1\):
$$ f(x) = x * x $$
Let’s use the idea of a fixed-point function to help solve our addition problem using recursion. We already know how to use a function in lambda calculus: function application. Application involves substituting a function’s bound variables (arguments) with argument expressions and evaluating the function’s body. You can delay this application by wrapping your function in another function. For example,
The function
$$ f : a $$
is equivalent to the following function
$$ \lambda g . (g : a) : f $$
where the original function \(f\) becomes the argument of a new function application in the body of \(g\) — when \(g\) is applied, the return value is \(f\ a\). By using \(g\) in place of \(f\) in a recursive function, we can substitute the recursive call with a new function that does not recurse. Rather it applies the recursion at the correct point in time using function application.
In general, the \(Y\) combinator function is used to create a recursive version of a function. It is a function that will return a fixed-point for any input function \(f\). When used as a function constructor, it creates a fixed-point over the argument that, when applied recurses. The \(Y\) combinator is defined as:
$$ Y=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)) $$
Applying the \(Y\) combinator gives,
$$ \begin{aligned} Y \ g &= (\lambda f.(\lambda x.f \ (x \ x)) (\lambda x.f \ (x \ x))) \ g & (\text{by definition}) \cr &= (\lambda x.g \ (x \ x)) (\lambda x.g \ (x \ x)) & (\text{by function application of } \lambda f) \cr &= g((\lambda x.g \ (x \ x)) (\lambda x.g \ (x \ x))) & (\text{by function application of } \lambda x.g(x \ x) \text{ to argument } \lambda x.g(x \ x)) \cr &= g\ (Y\ g) & (\text{by the second equality we just defined}) \end{aligned} $$
By repeatedly applying this equality we get,
$$ Y\ g=g\ (Y\ g)=g\ (g\ (Y\ g))=g\ (\ldots g\ (Y\ g)\ldots ) $$
Recursion is thus achieved by ensuring that a copy of the function’s argument and the self-application of the function, will continue with each application.
Applying the Y Combinator to add
Let’s return to our original problem add:
def add x y =
if iszero y
then x
else add (succ x) (pred y)
and define a recursive version of this function that takes the recursion
point as a parameter. This transformation is a quick slight-of-hand to
make the function usable as a input to the \(Y\) combinator. In general, for
a recursive function name:
def <name> = ... (<name ...>) ...
you can an alternate version with the recursion point as a function parameter by introducing a helper function as an argument to the $Y$ combinator:
def <name1> f = ... (f ...) ...
def <name> = Y <name1>
For the case of add, or function becomes:
def add f x y =
if iszero y
then x
else f (succ x) (pred y)
We can then feed this revised add function to the \(Y\) combinator and
evaluate it using the regular rules of lambda calculus.
$$ \begin{aligned} & Y \ \text{add} \ & (\text{by the equality derived above}) \cr &= \text{add}\ (Y\ \text{add}) & (\text{by substitution}) \cr &= \lambda f.\lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ f\ (\text{succ}\ x)\ (\text{pred}\ y))\ (Y\ \text{add}) & (\text{by substitution}) \cr &= \lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ (Y\ \text{add}) (\text{succ}\ x)\ (\text{pred}\ y))\ & \end {aligned} $$
This form of the function takes two parameters, \(x\) and \(y\). We can make this concrete by evaluating the function with concrete values \(1\) and \(1\).
$$ \begin{aligned} & \lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ (Y\ \text{add}) (\text{succ}\ x)\ (\text{pred}\ y))\ 1\ 1 & (\text{by susbstitution}) \cr & = (\text{if iszero}\ 1\ \text{then}\ 1\ \text{else}\ (Y\ \text{add}) (\text{succ}\ 1)\ (\text{pred}\ 1)) & (\text{applying succ and pred}) \cr & = (\text{if iszero}\ 1\ \text{then}\ 1\ \text{else}\ (Y\ \text{add})\ 2\ 0) & (\text{following else branch}) \cr & = (Y\ \text{add})\ 2\ 0 & \end{aligned} $$
This brings us back to our original equation with new parameters. That is, we started with \(Y\ add\ 1\ 1\), used the definition of the \(Y\) combinator to turn that into an equivalent problem \(add\ (Y\ add)\ 1\ 1\), and derived \(Y\ add\ 2\ 0\) using the rules of lambda calculus:
$$ \begin{aligned} & Y\ \text{add}\ 1\ 1\ & (\text{through equality}) \cr & = \text{add}\ (Y\ \text{add}) & (\text{by evaluation}) \cr & = Y\ \text{add}\ 2\ 0\ & \end{aligned} $$
We can continue our evaluation from this point to get our final answer for adding one and one:
$$ \begin{aligned} & \lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ (Y\ \text{add}) (\text{succ}\ x)\ (\text{pred}\ y))\ 2\ 0 & (\text{by susbstitution}) \cr & = (\text{if iszero}\ 0\ \text{then}\ 2\ \text{else}\ (Y\ \text{add}) (\text{succ}\ 2)\ (\text{pred}\ 0)) & (\text{applying succ and pred}) \cr & = (\text{if iszero}\ 0\ \text{then}\ 2\ \text{else}\ (Y\ \text{add})\ 3\ {-1}) & (\text{following then branch}) \cr & = 2 \end{aligned} $$
We’ve successfully applied the \(Y\) combinator to recursively add two numbers! I’ll conclude by putting the following steps together into one continuous equation:
$$ \begin{aligned} & Y\ \text{add}\ 1\ 1\ \cr & = \text{add}\ (Y\ \text{add})\ 1\ 1\ \cr & = \lambda f.\lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ f\ (\text{succ}\ x)\ (\text{pred}\ y))\ (Y\ \text{add})\ 1\ 1\ \cr & = \lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ Y\ \text{add} (\text{succ}\ x)\ (\text{pred}\ y))\ 1\ 1\ \cr & = (\text{if iszero}\ 1\ \text{then}\ 1\ \text{else}\ Y\ \text{add} (\text{succ}\ 1)\ (\text{pred}\ 1)) \cr & = (\text{if iszero}\ 1\ \text{then}\ 1\ \text{else}\ Y\ \text{add}\ 2\ 0) \cr & = Y\ \text{add}\ 2\ 0 \cr & = \text{add}\ Y\ \text{add}\ 2\ 0\ \cr & = \lambda f.\lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ f\ (\text{succ}\ x)\ (\text{pred}\ y))\ Y\ \text{add}\ 2\ 0\ \cr & = \lambda x.\lambda y.(\text{if iszero}\ y\ \text{then}\ x\ \text{else}\ Y\ \text{add} (\text{succ}\ x)\ (\text{pred}\ y))\ 2\ 0 \cr & = (\text{if iszero}\ 0\ \text{then}\ 2\ \text{else}\ Y\ \text{add}\ (\text{succ}\ 2)\ (\text{pred}\ 0)) \cr & = (\text{if iszero}\ 0\ \text{then}\ 2\ \text{else}\ Y\ \text{add}\ 3\ {-1}) \cr & = 2 \end{aligned} $$