Equational derivations of the Y combinator and Church encodings in Python

What is lambda?

Lambda is a notation for expressing anonymous functions.

For instance, in Python, we define the function f using def:

def f(x):
  return x + 1

print (f(10))    # prints 11

Or, we can assign f to lambda x: x + 1:

f = lambda x: x+1

print (f(10))   # prints 11

The lambda calculus

Alonzo Church discovered the lambda calculus back in the 1920s, not as a programming language, but in an effort to find a functional foundation for logic.

The lambda calculus is what’s left of mathematics if you take away everything except for variables, anonymous functions (lambdas) and function application.

It’s also the world’s smallest universal programming language, and it lives inside many major programming languages these days, including Python, JavaScript, Ruby, PHP, Java and C++. (Of course, it also lives in the functional languages.)

The following grammar carves out a subset of Python that encodes the lambda calculus:

 <exp> ::= <var>
        |  <exp>(<exp>)
        |  lambda <var>: <exp>
        |  (<exp>)

 <var> is a legal variable name

In the lambda calculus, all values are functions.

A programming language out of lambda

At first glance, the lambda calculus doesn’t appear to be a universal foundation for programming.

To convert it into a universal foundation, we will steadily construct the features expected of a modern programming language:

• void values;
• multi-argument functions;
• booleans and conditionals;
• numbers and arithmetic;
• pairs;
• lists; and
• recursive functions.

To do this, we’ll employ lambda-based programming techniques such as Currying, Church encodings, self-application, eta-expansion and the fixed-point combinators.

A void value

Sometimes, we’ll need a “void” value that we can pass when we expect that argument to be ignored.

We’ll the identity function to accomplish this;

VOID = lambda void: void

If we wanted ‘debugging’ support for this development, you might want to temporarily use an alternate definition of VOID:

def VOID(_): 
  raise Exception('Cannot invoke VOID!') 

In this case, if someone accidentially invokes VOID, it will blow up.

Multi-argument functions

The lambda calculus requires that every function have exactly one argument.

It’s easy to see how to fake zero-argument functions: we can take every call with zero arguments:

f()

and convert it into a call that takes VOID:

f(VOID)

so that every lambda taking zero arguments:

lambda : body

becomes a lambda with an ignored argument:

lambda _ : body

If we want true multi-argument functions, we need to use Currying.

In the case of a function over two arguments, the Curried function becomes a function that accepts the first argument, but then returns a function accepting the second argument and returning the result.

For example, suppose we have a function sum:

sum = lambda x, y: x + y

print (sum(2,3))     # prints 5

we could Curry it to produce a function that completes the sum:

sum = lambda x: lambda y: x + y

print (sum(2)(3))    # prints 5

At this point, we can desugar multi-argument functions into strictly single-argument functions.

Conditionals and Booleans

To develop conditionals, we want to create a function that simulates the behavior of the classic McCarthy-style if <condition> then <exp> else <exp> construct.

In C-like languages, this construct is the ternary operator:

  <condition> ? <exp> : <exp>

and in Python proper, this is

  <exp> if <condition> else <exp>`

To start, we’re going to constrain the function IF and the values TRUE and FALSE so that:

IF (TRUE)  (true_value) (false_value) == true_value
IF (FALSE) (true_value) (false_value) == false_value

There are several ways to do this, but we can take a step in the right direction by remembering that all values in the lambda calculus are functions – including whatever TRUE and FALSE must be.

Then, we can constrain IF to be the function that applies the condition to its arguments:

IF (cond) (true_value) (false_value) == cond(true_value)(false_value)

which leads to a pure-lambda definition of IF:

IF = (lambda cond: lambda true_value: lambda false_value:
       cond(true_value)(false_value))

At this point, we can equationally solve for the definition of TRUE and FALSE:

    TRUE (true_value) (false_value)
 == IF (TRUE) (true_value) (false_value) 
 == true_value

And, as before, we can turn this into a valid Python definition by moving the arguments with lambdas:

TRUE = lambda true_value: lambda false_value: true_value

Following the same process for FALSE yields:

FALSE = lambda true_value: lambda false_value: false_value

Making it work with eager languages

This encoding for TRUE and FALSE works when the computations for the true branch and the false branch are terminating and error-free.

But, if we tried IF (TRUE) (value) (nonterminate()) where nonterminate() never completes, then the result will not be equal to value, because the entire expression will never terminate.

To fix this, we must “thunk” the arguments to IF by wrapping them in lambdas to suspend their computation:

IF (TRUE)  (lambda: true_value)  (lambda: false_value) == true_value
IF (FALSE) (lambda: false_value) (lambda: false_value) == false_value 

The definition of IF stays the same, but resolving for TRUE and FALSE yields:

TRUE  = lambda true_value: lambda false_value: true_value()
FALSE = lambda true_value: lambda false_value: false_value()

Numbers

Church numerals are a means for encoding the natural numbers as functions.

In the spirit of encoding data as its use, Church numerals encode natural numbers as iterated application.

For example, the Church numeral for 3 is a function that applies a composes its argument with itself 3 times.

That means that ZERO, given any function, returns the identity function:

ZERO (f) (z) == z

so that:

ZERO = lambda f: lambda z: z

The Church numeral for ONE applies its argument once; TWO applies it twice; THREE applies it three times:

ONE   (f) (z) == f(z)
TWO   (f) (z) == f(f(z))
THREE (f) (z) == f(f(f(z)))

so that:

ONE   = lambda f: lambda z: f(z)
TWO   = lambda f: lambda z: f(f(z))
THREE = lambda f: lambda z: f(f(f(z)))

Alternatively, if we define function composition, compose:

compose = lambda f,g: lambda x: f(g(x))

we can represent these numbers in a point-free style:

ONE   = lambda f: f
TWO   = lambda f: compose(f,f)
THREE = lambda f: compose(f,compose(f,f))

We can write a function in Python that turns a Python number into a Church numeral:

def numeral(n):
  return lambda f: lambda z: z if n == 0 else f(numeral(n-1)(f)(z))

print (numeral(0)(lambda x: x+1)(0))   # prints 0
print (numeral(7)(lambda x: x+1)(0))   # prints 7
print (numeral(3)(lambda x: 2*x)(1))   # prints 8

and a function that turns a Church numeral back into a number:

natify = lambda c: c(lambda x: x+1)(0)

print (natify (ONE))  # prints 1
print (natify (TWO))  # prints 2

Successors

Given the representation of a Church numeral, \(n\), its successor, \(n+1\) should apply f one more time:

SUCC (n) (f) (z) == f(n(f)(z))

By pulling the arguments across with lambda, we get a definition for SUCC:

SUCC = lambda n: lambda f: lambda z: f(n(f)(z))

And, it works:

print (SUCC (ONE) (lambda x: x+1) (0)) # prints 2

Addition

To add \(n\) and \(m\) as Church numerals, we want to apply a function \(n\) times and then apply it \(m\) times.

So, we can define addition using composition:

SUM (n) (m) (f) (z) == compose(n(f),m(f))(z)

so that:

SUM (n) (m) (f) == compose(n(f),m(f))

and using lambdas to peel off the arguments:

SUM = lambda n: lambda m: lambda f: compose(n(f),m(f))

And, after inlining the compose:

SUM = lambda n: lambda m: lambda f: lambda z: n(f)(m(f)(z))

A few tests show that it works:

FOUR = SUM (TWO) (TWO)
FIVE = SUM (TWO) (THREE)

print (natify (FOUR))  # prints 4
print (natify (FIVE))  # prints 5

Multiplication

To multiply \(n\) and \(m\) as Church numerals, we want to apply the encoding of \(n\) exactly \(m\) times:

MUL (n) (m) (f) (z) == m(n(f))(z)

so that peeling the arguments off with lambdas yields:

MUL = lambda n: lambda m: lambda f: lambda z: m(n(f))(z)

And, we can even derive a point-free version with compose:

MUL = lambda n: lambda m: lambda f: lambda z: m(n(f))(z)
    = lambda n: lambda m: lambda f: m(n(f))
    = lambda n: lambda m: lambda f: compose(m,n)(f)
    = lambda n: lambda m: compose(m,n)

And, it works:

FOUR = MUL (TWO) (TWO)
SIX  = MUL (TWO) (THREE)

print (natify (FOUR))  # prints 4
print (natify (SIX))   # prints 6

Pairs

To create pairs (and tuples), we want a constructor that can create a pair (PAIR) and accessors to pull components out (LEFT, RIGHT).

Together, they need to obey the following properties:

LEFT  (PAIR (a) (b)) == a
RIGHT (PAIR (a) (b)) == b

Let’s assume that a pair is a function that applies its first argument to both the left and the right value:

PAIR (a) (b) == lambda f: f(a)(b)

so that:

PAIR = lambda a: lambda b: lambda f: f(a)(b)

Then we can solve for LEFT:

    a
 == LEFT (PAIR (a) (b))
 == LEFT (lambda f: f(a)(b))

Assuming LEFT (p) == p(g) for some unknown function g lets us solve for g:

    LEFT (lambda f: f(a)(b))
 == (lambda f: f(a)(b))(g)
 == g(a)(b)

All together, a == g(a)(b), so we can solve for g by pulling the arguments across with lambda:

g = lambda a: lambda b: a

which means that:

LEFT = lambda p: p(lambda a: lambda b: a)

Repeating the process for RIGHT yields:

RIGHT = lambda p: p(lambda a: lambda b: b)

Lists

To create lists, we need a NIL element, a list constructor CONS, a predicate for detecting empty lists NILP, a HEAD accessor and a TAIL accessor, so that all together, the following constraints hold:

NILP (NIL) == TRUE
NILP (CONS (hd) (tl)) == FALSE

HEAD (CONS (hd) (tl)) == hd
TAIL (CONS (hd) (tl)) == tl

To pull this off, we will allow a list to take two functions: one to call when the list is empty and the other to call when the list is non-empty.

Under this interpretation, NIL should call the empty function:

NIL = lambda onnil: lambda onlist: onnil()

And, the CONS constructor should call the non-empty function with both the head and the tail:

CONS (hd) (tl) == lambda onnil: lambda onlist: onlist(hd)(tl)

so that:

CONS = (lambda hd: lambda tl:
         lambda onnil: lambda onlist: onlist(hd)(tl))

Under this convention, NILP can engineer the functions it passes in to return the appropriate value:

NILP (list) == list (lambda: TRUE) (lambda hd: lambda tl: FALSE)

so that:

NILP = lambda list: list (lambda: TRUE) (lambda hd: lambda tl: FALSE)

And, at the same time HEAD and TAIL can extract the appropriate value:

HEAD = lambda list: list (VOID) (lambda hd: lambda tl: hd)
TAIL = lambda list: list (VOID) (lambda hd: lambda tl: tl)

Non-termination via the U Combinator

The first hint that the lambda calculus may be capable of general purpose computation comes from the U Combinator.

The U combinator is the function that applies its argument to itself:

U = lambda f: f(f)

When we apply the U Combinator to itself, something strange happens:

U(U)  # error: stack overflow!

Because Python lacks tail-call optimization, it blows out the call stack.

In languages with correct tail-call handling, it non-terminates.

In the context of U(U), the expression f ends up being bound to lambda f: f(f).

Through self-application, we achieved self-reference.

Recursion via the U Combinator

Once non-termination enters the picture, it’s natural to wonder if one might do more than just non-terminate.

Can we achieve recursion through self-application?

We can.

Consider the recursive definition of factorial:

fact = lambda n: 1 if n <= 0 else n*fact(n-1)

We can try to pass a copy of “factorial” into itself:

fact = ((lambda n: 1 if n <= 0 else n*fact(n-1))
        (lambda n: 1 if n <= 0 else n*fact(n-1)))

But, this doesn’t work: n ends up bound to (lambda n: 1 if n <= 0 else n*fact(n-1)), and the program breaks.

But, what if we add an extra parameter to represent the function itself?

We end up with:

fact = ((lambda f: lambda n: 1 if n <= 0 else n*fact(n-1))
        (lambda f: lambda n: 1 if n <= 0 else n*fact(n-1)))

Now, it works, but we still have a recursive reference to fact.

Fortunately, f(f) (or U(f)) will produce a new reference to fact.

So, we can use:

fact = ((lambda f: lambda n: 1 if n <= 0 else n*(U(f))(n-1))
        (lambda f: lambda n: 1 if n <= 0 else n*(U(f))(n-1)))

and clean the whole expression up with a call to the U combinator:

fact = U(lambda f: lambda n: 1 if n <= 0 else n*(U(f))(n-1))

Sure enough, it works:

U(lambda f: lambda n: 1 if n <= 0 else n*(U(f))(n-1))(5) # prints 120

Booleans. Numbers. Pairs. Lists. Recursion.

None are fundamental.

If we have anonymous functions, we have all of these.

Expressing recursion via the Y Combinator

The U Combinator may be sufficient to demonstrate the universality of the lambda calculus, but for those that wish to use the lambda calculus as an everyday programming language, it is cumbersome.

The Y Combinator is an elegant way to express recursive functions.

To express recursion via the Y Combinator requires two steps:

1. express a recursive function as the fixed point of a non-recursive function; and

2. create a function – the Y Combinator – to find the fixed point of another function, without using recursion.

The fixed point of a function \(f\) is the value \(x\) such that \(x = f(x)\).

A functional is a function that takes a function as its argument.

The fixed point of a functional (if it exists), by definition, would have to be a function.

To put this in more concrete terms, we can work on a specific example:

What is the functional for which factorial is a fixed point?

Let’s cheat at first, and assume we already have a recursive defintion of factorial available:

fact = lambda n: 1 if n <= 0 else n*fact(n-1)

A simple functional that returns factorial when given factorial is:

lambda f:fact

We can inline fact once to arrive at:

lambda f: lambda n: 1 if n <= 0 else n*fact(n-1)

Given factorial, the above will return factorial.

Under the assumption that factorial will be passed in for f, we can confidently state that the fixed point of the following functional is factorial:

lambda f: lambda n: 1 if n <= 0 else n*f(n-1)

What we need now is a function Y that will find the fixed point of a functional for us, so that:

fact = Y(lambda f: lambda n: 1 if n <= 0 else n*f(n-1))

Deriving the Y Combinator

To derive the Y Combinator, let us first state the key property we seek; Y(F) should return the fixed point of F:

Y(F) == f   and   f == F(f)

Substituting F(f) for f gives:

Y(F) == F(f)

Because f == Y(F), we can substiute for f yet again to yield:

Y(F) == F(Y(F))

We can pull the argument off with lambda to get an operational definition:

Y = lambda F: F(Y(F))

Of course, this won’t work:

Y(lambda f: lambda n: 1 if n <= 0 else n*f(n-1))(5) # stack overflow!

The problem is that Y immediately invokes Y recursively.

Fortunately, we can \(\eta\)-expand the call to Y, under the observation that for any expression in the lambda calculus, e:

e == lambda x: e(x)

except that if e is non-terminating, then the expanded expression will terminate.

This expansion yields a new definition of Y:

Y = lambda F: F(lambda x:Y(F)(x))

And, already, this works:

Y(lambda f: lambda n: 1 if n <= 0 else n*f(n-1))(5) # prints 120

All that’s left now is to apply the U combinator to eliminate the explicit recursion in the definition of Y:

Y = U(lambda h: lambda F: F(lambda x:U(h)(F)(x)))

And, of course, we can also inline U to leave an expression in the pure lambda calculus:

Y = ((lambda h: lambda F: F(lambda x:h(h)(F)(x)))
     (lambda h: lambda F: F(lambda x:h(h)(F)(x))))

Observe:

Y(lambda f: lambda n: 1 if n <= 0 else n*f(n-1))(5) # prints 120

All together

Putting together all of the Church encodings and the Y Combinator allows the expression of factorial in pure lambda calculus, in which case fact(5) becomes:

(((lambda f: (((f)((lambda f: ((lambda z: (((f)(((f)(((f)(((f)(((f)
(z)))))))))))))))))))((((((lambda y: ((lambda F: (((F)((lambda x:
(((((((y)(y)))(F)))(x)))))))))))((lambda y: ((lambda F: (((F)((lambda x:
(((((((y)(y)))(F)))(x)))))))))))))((lambda f: ((lambda n: ((((((((((((
lambda n: (((((n)((lambda _: ((lambda t: ((lambda f: (((f)((lambda void:
(void)))))))))))))((lambda t: ((lambda f: (((t)((lambda void: (void)))))
))))))))((((((lambda n: ((lambda m: (((((m)((lambda n: ((lambda f:
((lambda z: (((((((n) ((lambda g: ((lambda h: (((h)(((g)(f)))))))))))
((lambda u: (z)))))((lambda u: (u)))))))))))))(n))))))) (n)))((lambda f:
((lambda z: (z)))))))))((lambda _: ((((lambda n: (((((n) ((lambda _: ((
lambda t: ((lambda f: (((f)((lambda void: (void))))))))))))) ((lambda t:
((lambda f: (((t)((lambda void: (void))))))))))))) ((((((lambda n: 
((lambda m: (((((m)((lambda n: ((lambda f: ((lambda z: (((((((n) ((lambda
g: ((lambda h: (((h)(((g)(f)))))))))))((lambda u: (z)))))((lambda u:
(u)))))))))))))(n)))))))((lambda f: ((lambda z: (z)))))))(n)))))))))
((lambda _: ((lambda t: ((lambda f: (((f)((lambda void: (void)))))))))))
))((lambda _: ((lambda f: ((lambda z: (((f)(z)))))))))))((lambda _: (((
(((lambda n: ((lambda m: ((lambda f: ((lambda z: (((((m)(((n)(f)))))(z)
))))))))))(n)))(((f) ((((((lambda n: ((lambda m: (((((m)((lambda n:
((lambda f: ((lambda z: (((((((n) ((lambda g: ((lambda h: (((h)(((g)(f)
))))))))))((lambda u: (z)))))((lambda u: (u)))))))))))))(n)))))))(n)))
((lambda f: ((lambda z: (((f) (z))))))))))))))))))))))))(lambda x:x+1)(0)

Code

A condensed version of the code in this post is available.

More reading

• Barendregt is still the classic tome:
  

Exercises

1. Write PRED to return the predecessor of a Church numeral.

---