Lambda Calculus - Recursion

In computer science recursion is the act of solving a problem with intermediate results of smaller instances of the same problem. A function used to solve a problem is therefore calling itself within its own definition. This concept is usually supported by most programming languages in addition to the imperative style of programming, which uses control structures such as for and while loops. Some functional programming languages even support recursion as the only method of problem solving. This article is about the definition of recursion in lambda calculus.

Anonymous functions

A recursive function is defined in terms of the function itself. In lambda calculus all functions are anonymous, they are not given explicit names.

Although it is common to have equivalent function names for specific lambda terms in the form

$$ \text{\small MULT} \equiv \lambda xyz.x(yz)\text{,} $$

it is important to understand that this is not part of the lambda calculus syntax. Equivalent function names are only there to make the notation easier. In the formal system lambda calculus there is no operation to assign names to lambda terms. In order to be able to express recursion, the concept of a fixed point has to be used.

Fixed points

A fixed point of a function is an element of its domain which is mapped to itself. For example: For a given function

$$ f: X \to X $$

the element $a\in X$ is considered the fixed point of $f$ if $f(a)=a$.

An example of fixed points can be given with the factorial function, notated as $n!$, which returns the product of all positive integers $\leq n$. The fixed points for the factorial function are:

$$ f(0) = 1 \newline f(1) = 1 \newline f(2) = 2 $$

Transferring the concept of fixed points to lambda calculus means, that a lambda term $M Q$ can be reduced to

$$ MQ = Q \text{.} $$

Here, $M$ is a function mapping lambda terms to lambda terms

$$ M: \varLambda \to \varLambda $$

with $\varLambda$ representing all lambda terms and $Q$ any fixed point of $M$.

How is it possible to utilize fixed points regarding the definition of recursion in lambda calculus?

Recursive addition

Let’s examine the addition function $\text{\small ADD}$, which was already expressed in terms of the successor function $\text{\small SUCC}$ in a previous post. The recursive definition of addition looks like this:

$$ \text{\small ADD } x \thinspace y\equiv \begin{cases} x &\text{if } y=0 \cr \text{\small SUCC }(\text{\small ADD } x \thinspace (\text{\small PRED }y)) &\text{if otherwise} \end{cases} $$

To give an example:

$$ \begin{aligned} \text{\small ADD } 2 \thinspace 2 &= \text{\small SUCC }(\text{\small ADD } 2 \thinspace 1) \cr &= \text{\small SUCC }(\text{\small SUCC } (\text{\small ADD } 2 \thinspace 0)) \cr &= \text{\small SUCC }(\text{\small SUCC } 2) \cr &= 4 \end{aligned} $$

Testing for the value zero was introduced in a previous article. Therefore, a recursive definition of addition in lambda terms could look like this:

$$ \text{\small ADD } \equiv \lambda xy.Z\thinspace y \thinspace x \thinspace \text{\small SUCC}((\text{\small ADD } x\thinspace (\text{\small PRED } y))) $$

Unfortunately, this definition is using $\text{\small ADD}$ before it was defined! For a valid lambda expression $\text{\small ADD}$ has to appear in the function’s head.

This can be done with abstracting over $\text{\small ADD}$ using a function $\text{\small ADD}'$:

$$ \text{\small ADD}' \equiv \lambda \thinspace \text{\small ADD }xy.Z\thinspace y \thinspace x \thinspace \text{\small SUCC}((\text{\small ADD } x\thinspace (\text{\small PRED } y))) $$

The function $\text{\small ADD}'$ is now accepting the actual addition function as a parameter along with the two arguments we want to add together.

To now get our real addition function the fixed point of $\text{\small ADD}'$ has to be found:

$$ \text{\small ADD}' \thinspace \text{\small ADD} = \text{\small ADD} $$

How is it possible to find a fixed point of a lambda expression?

The Y combinator

In lambda calculus a theorem states that each lambda term has at least one fixed point (see Barendregt and Barendsen), which can be found using fixed point operators. One of these operators, the combinator $Y$, was found by Haskell B. Curry.

The $Y$ combinator is defined as:

$$ Y \equiv \lambda f.(\lambda x.f(xx))(\lambda x.f(xx)) $$

Given an arbitrary argument $G$ the combinator returns:

$$ \begin{aligned} YG &\equiv \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))\thinspace G \cr &= (\lambda x.G(xx))(\lambda x.G(xx)) \cr &= G((\lambda x.G(xx))(\lambda x.G(xx))) \cr &= G(YG) \end{aligned} $$

In other words: For every lambda term $G$, $(YG)$ is a fixed point of $G$.

The $Y$ combinator can therefore be used to find the fixed point of a given lambda expression if it exists. The simplest demonstration can be given with the function

$$ \lambda x.T $$

that returns the true value $T$ for any given argument. Obviously, the fixed point of this function is $T$:

$$ \begin{aligned} Y(\lambda x.T) &= \lambda x.T(Y\thinspace \lambda x.T) \cr &= T \end{aligned} $$

The $Y$ combinator is used to create recursive functions. This can be visualized by the repeated application of $YG$:

$$ YG = G(YG) = G(G(YG)) = … $$

Revisiting recursive addition

The lambda term which defines the addition function $\text{\small ADD}$ can now be expressed using the $Y$ combinator:

$$ \begin{aligned} \text{\small ADD} &\equiv Y\text{\small ADD}' \cr &= Y(\lambda \thinspace \text{\small ADD }xy.Z\thinspace y \thinspace x \thinspace \text{\small SUCC}((\text{\small ADD } x\thinspace (\text{\small PRED } y)))) \end{aligned} $$

The example $1+1$ can be evaluated to:

$$ \begin{aligned} \text{\small ADD } 1 \thinspace 1 &\equiv (Y\text{\small ADD}')\thinspace 1 \thinspace 1 \cr &= (\text{\small ADD}' (Y \text{\small ADD}'))\thinspace 1 \thinspace 1 \cr &= (\lambda \thinspace \text{\small ADD }xy.Z\thinspace y \thinspace x \thinspace \text{\small SUCC}((\text{\small ADD } x\thinspace (\text{\small PRED } y)))) (Y\text{\small ADD}') \thinspace 1 \thinspace 1 \cr &= (\lambda xy.Z\thinspace y \thinspace x \thinspace \text{\small SUCC}((Y\text{\small ADD}')\thinspace x \thinspace (\text{\small PRED } y)))) \thinspace 1 \thinspace 1 \cr &= Z\thinspace 1 \thinspace 1 \thinspace \text{\small SUCC}((Y\text{\small ADD}') 1\thinspace (\text{\small PRED } 1))) \cr &= \text{\small SUCC}((Y\text{\small ADD}') \thinspace 1\thinspace 0) \cr &= \text{\small SUCC}(Z\thinspace 0 \thinspace 1 \thinspace (Y\text{\small ADD}') \thinspace 1\thinspace (\text{\small PRED } 0)) \cr &= \text{\small SUCC}(Z\thinspace 0 \thinspace 1 \thinspace (Y\text{\small ADD}') \thinspace 1\thinspace (\text{\small PRED } 0)) \cr &= \text{\small SUCC}(1) \cr &= 2 \cr \end{aligned} $$

Example implementation

It was stated that lambda calculus can not express recursion in a straightforward manner, as all functions are anonymous. Using the $Y$ combinator, the process of creating recursive definitions nonetheless looks like this:

Define a recursive function
Create an abstraction of this function which takes the recursive function itself as an argument
Use the $Y$ combinator to evaluate this function

The $Y$ combinator therefore potentially allows the implementation of recursion in programming languages which do not explicitly support this feature. Of course, since almost every programming language can make use of recursion in some way, this is an interesting but more of an academic use case.

How to implement the combinator and use it to define a recursive version of the addition function is demonstrated below. Due to its functional nature and its clear syntax, the programming language GNU R is being used. Being a dynamically typed language is also beneficial as realizing the $Y$ combinator in a statically typed language is usually a bit more cumbersome.

# Y combinator based on the expression:
#
# Y = λf.(λx.f(xx))(λx.f(xx))
Y <- function(f) {
  fxx <- function(x) { f((x)(x)) } 
    
  (fxx)(fxx)
}

# Abstracted addition function expecting
# the real addition function as a parameter.
# Based on the expression:
#
# λ ADD xy.Z y x SUCC((ADD x (PRED y)))
add_generator <- function(add) {
  function(x,y) {
    if (y == 0) {
      x
    } else {
      add(x,y-1) + 1
    }
  }
}

# Extract our real addition function as the fixed 
# point of add_generator.
add <- function(x,y) { Y(add_generator)(x,y) }

# Example application
print(add(2,2))

For a quick validation that this code works, an online R compiler can be used.