Understanding Church numerals

The lambda calculus syntax is so simple that it can be defined in the following three rules:

1. A variable \(x\) is a character or string that represents a parameter.
2. A lambda abstraction \((\lambda x. M)\) defines an anonymous function, with a parameter \(x\) (between the λ and the dot), that returns the body \(M\).
3. An application \((M\ N)\), where the function \(M\) is called with \(N\) as its argument.

In a function application, \(M\) and \(N\) are lambda terms. A lambda terms is simply a valid expression in the lambda calculus system. To determine if an expression is valid, the following three rules can be used:

1. A variable \(x\) is itself a valid lambda term.
2. If \(M\) is a lambda term, and \(x\) is a variable, then \((\lambda x. M)\) is also a lambda term.
3. If \(M\) and \(N\) are lambda terms, then \((M\ N)\) is also a lambda term.

The recursive nature of λ-calculus is present in the definition of the syntax itself, where:

• Variables provide a way of naming an unknown lambda term.
• Lambda abstractions provide a way of extracting part of a lambda term.
• Applications provide a way of filling a variable, which was extracted/abstracted, with new a lambda term (the argument of the application).
• Lambda terms themselves are any of the above.

At first glance, a system that doesn’t directly deal with specific data (such as numbers) may seem pointless, but it has helped shape many modern languages, and understanding how to use these simple rules in these complex systems can be extremely helpful.

Since λ-calculus doesn’t deal with specific values such as numbers, the value of the system lies in the way lambda terms can be transformed.

Before diving into the transformation methods, it’s important to mention the substitution notation that is often used in this context. An expression like \(b[p := a]\), denotes the operation of substituting the parameter \(p\) with the argument \(a\) in the body \(b\). Similarly, the syntax \(M[x]\) is used to denote “a lambda expression \(M\) which contains a bound variable \(x\)”.

There are three kinds of transformations, which are used to convert lambda expressions to equivalent ones.

Alpha conversion (α-conversion)

Consists on renaming the bound variables in an expression. It is mainly used to avoid name collisions.

\[ (\lambda x. M[x]) \to (\lambda y. M[y]) \]

Beta reduction (β-reduction)

Consists on reducing an application by substituting the bound variable in the body of the abstraction with the argument of the application. Essentially, applying a function call.

\[ ((\lambda x. M)\ N) \to M[x := N] \]

In this case, the reduction consists on substituting \(x\) in the body \(M\) with \(N\).

The inverse of this process is called beta abstraction, which instead of simplifying an expression, adds an extra function call. This can be useful in languages such as Lisp for delaying the evaluation of the arguments.

\[ M[N] \to ((\lambda x. M)\ N) \]

Eta reduction (η-reduction)

Expresses the idea of extensionality, which applied to this context establishes that two functions are the same if and only if they give the same result for all arguments.

It is used to simplify redundant abstractions; for example, given that \(x\) does not appear free in \(f\):

\[ (\lambda x. f\ x) \to f \]

The inverse of this process is called eta expansion, which essentially wraps a function into a lambda abstraction:

\[ f \to (\lambda x. f\ x) \]

These transformations can be used to transform computations into simpler and more efficient ones.

Finally, to fully understand λ-notation, there are some conventions that should be kept in mind when it comes to notation.

• Outermost parentheses are dropped: \((M N)\) can be noted as \(M N\).
• Applications are assumed to be left associative: \(M N P\) is equivalent to \(((M N) P)\), instead of \((M (N P))\).
• The body of an abstraction extends as far right as possible: \((\lambda x. M N P)\) means \((\lambda x. (M N P))\), instead of \(((\lambda x. M) N P)\) or \(((\lambda x. M N) P)\).
• A sequence of abstractions can be contracted: \((\lambda x. \lambda y. \lambda z. N)\) can be expressed as \((\lambda x\ y\ z. N)\). This is related to the notion of currying.
• When all variables are single-letter, the space in applications may be omitted: \((xyz)\) instead of \((x\ y\ z)\).

For the sake of readability, this article will intentionally avoid using some of these conventions (e.g. dropping outermost parentheses), specially for the expressions embedded in text.

This is the definition of add-1 in λ-notation¹.

\[ \lambda n. \lambda f. \lambda x. f (n\ f\ x) \]

This is the equivalent definition of add-1 in Lisp.

(define add-1
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (f ((n f) x))))))

A call to add-1 with an argument of zero can be examined through β-reduction to understand why the Church numeral for one is returned. Each step of the reduction will be highlighted and explained using Lisp syntax.

First, the call to add-1 is expanded, replacing each symbol with its bound expression.

Then, the outermost call is evaluated, replacing the n parameter in the body of add-1 with the value of zero. Specifically, to avoid naming collisions, n is replaced with the α-conversion of zero, where the f and x symbols are substituted with g and y, respectively.

Once the outer call has been evaluated, the expression can be simplified by evaluating the call to zero, that is, the call to the lambda whose parameter is y, and whose argument is f. Since the parameter g does not appear in the body, is is essentially discarded, resulting in (lambda (y) y), the identity function.

Finally, the call to the identity lambda can be evaluated, that is, the call to the lambda whose parameter is z and whose argument is x. A call to this function simply evaluates to the argument, in this case, x.

This final expression matches the definition of one from the previous section: a function that receives a function f, and returns another function that applies f to its argument x.

Naturally, the same β-reduction process can be expressed in λ-notation.

The same process can be done to β-reduce a call to add-1 with an argument of one. From the previous definitions:

The following β-reduction process can be performed:

The initial expression \(\eqref{eq:definition}\) is simply the call to add-1, replacing the symbols with the values defined above. Then, the call is β-reduced in \(\eqref{eq:reduction}\) by replacing the parameter \(n\) with the argument one, which was α-converted to avoid parameter collisions, just like in the example from the previous section. The call to the innermost lambda is β-reduced in \(\eqref{eq:reduction2}\) produce \((\lambda y. f\ y)\), that is, a function that applies \(f\) to its argument. Finally, the call to that lambda, whose argument is \(x\), is also reduced into \((f\ x)\); this result \(\eqref{eq:solution}\) matches the previous definition of two.

From the previous expressions, it can be concluded that the new addition function should essentially replace x (in either expression, since addition is commutative) with the entire body of the other expression’s innermost lambda. This abstract process is represented in the following figure, which shows the expected behavior when adding the Church numeral representation of 2 and 3.

For simplicity, this approach will be used for the rest of the section, where the body of the first argument a is “placed” in the second argument b.

Since the parameters of add are known, its initial structure can be defined. The following figure shows the partial definition, which will evolve trough this section.

Since the function will manipulate the bodies of the innermost lambdas, it must be able to access them. Specifically, it needs to:

1. Extract the innermost body from a, that is, (f (f x)).
2. Replace x in the innermost body of b.

It might be easier to understand this process by first examining the second step, the replacement of x.