The predecessor function for Church Numerals in the Lambda Calculus

In the 1920's and 30's, Alonzo Church and colleagues were experimenting
with alternatives to set theory as a basis for mathematics [Cardone].
They explored an approach that used functions as the bedrock on which to
build the rest of mathematics, as opposed to sets. They formalized their
approach with a notation they named lambda calculus. The intention was
that functional reasoning and the lambda calculus could express all of
mathematics, in a manner similar to set theory.

For this to be true, it is of course necessary that the integers be
representable. A cute technique now referred to as Church numerals
served this purpose. It turned out to be a simple matter to express
most of the standard operations over the integers using Church numerals;
addition, multiplication, exponentiation for example. However, Church and
his students were initially unable to figure out how to do subtraction!
Any system that purports to be universal in some sense for mathematics
that cannot do subtraction is not going to get too far..

Steven Kleene devised a clever encoding in the new lambda calculus
notation for the predecessor function over integers as represented by
Church numerals. With predecessor in hand, it became a simple matter
to derive subtraction and division.

Looking at the usual minimalistic, normalform presentation of the
predecessor function in lambda calculus is a bit like trying to understand
the quicksort algorithm by looking at a hexadecimal machine dump.
It is zenlike in its minimality and opacity to the unenlightened.

The intent of this note is to create an onramp to the predecessor
function. This goal seems not to be easily achievable, as evidenced
by the many attempts already on the net that IMHO do not achieve it.
You read these sites and say "WHAT?!? More incomprehensible gibberish
involving Greek letters.."

So, let's get started and see if this attempt will be any better.
I will use lua 5.1 as the programming notation, so that everything can
be copied and pasted into an interactive lua interpreter and executed.

Here are the first three Church numerals expressed in lambda calculus,
encoding zero, one, and two:

λ s . λ z . z
λ s . λ z . s(z)
λ s . λ z . s(s(z))
Transliterating to lua, and allowing multiple arguments, we can express
these lambda terms as follows:

Zero =
function(next, first)
return first
end
One =
function(next, first)
return next(first)
end
Two =
function(next, first)
return next(next(first))
end
It is easy to see what is going on. Each functional encoding of an
integer N takes two arguments: a function "next" and an arbitrary value
"first". The encoded integer simply applies "next()" to "first" to get
a result, applies "next()" to this result, and repeats. The encoding of
the nonnegative integer N iterates this process N times. (The "next()"
function must of course return a value that is of the same type as
its input.)

So, in the lambda calculus we have a countably infinite set of lambda
terms, all in normal form, and all distinct. This scheme turns out to be
a convenient representation of the nonnegative integers.

It is important to note that a Church numeral can be applied to any
function and value, and we will exploit this fact ruthlessly in what
follows. To get a feel for things, let us create a little utility
function that maps our Church numerals to actual integers in lua.

ToInteger =
function(church_numeral)
local next =
function(n)
return n + 1
end
local first = 0
return church_numeral(next, first)
end
We can fire up the lua interpreter, copy and paste the definitions above,
and then use them:

> print(ToInteger(Zero))
0
> print(ToInteger(One))
1
> print(ToInteger(Two))
2
It is easy to write an Increment function that takes a number and returns
the encoding of the next larger integer, by simply applying the "next"
argument one extra time:

Increment =
function(church_numeral)
local result =
function(next, first)
return next(church_numeral(next, first))
end
return result
end
The Add function is similarly straightforward:

Add =
function(church_numeral1, church_numeral2)
local result =
function(next, first)
return church_numeral1(next, church_numeral2(next, first))
end
return result
end
Multiply =
function(church_numeral1, church_numeral2)
local result =
function(next, first)
local add_church_numeral1 =
function(n)
return church_numeral1(next, n)
end
return church_numeral2(add_church_numeral1, first)
end
return result
end
Now, on to the main event, the predecessor function. This function
is given a Church numeral C_{N} corresponding to the integer
N, and is supposed to return another Church numeral C_{N1},
corresponding to the integer N1.

The resulting function C_{N1} will have to make use of its
argument C_{N} somehow, and the only thing the latter knows
how to do is apply a function "next" N times to a "first" value. So we
have to cook up a new function and a new value. When the new function is
applied N times to the new value, it must have the effect of applying the
original "next" function only N1 times to the original "first" value.

The idea is to create a new "pred_next" function and "pred_first" value
and have them use the original "next" function and "first" value in a
clever way.

The "pred_first" value will be an ordered pair

{ true, first }
The "pred_next" function uses the first boolean value to decide whether to
"skip" an application of the "next" function:

{ true, first } > { false, first }
{ false, first } > { false, next(first) }
{ false, next(first) } > { false, next(next(first)) }
...
When we have applied this "pred_next" function N times, we fish out the
second component of the last ordered pair, and this is our desired result
of applying the successor function N1 times.

Here is an encoding of this idea in lua:

Pred =
function(church_numeral)
local result =
function (next, first)
local pred_first =
{ skip_next = true, value = first }
local pred_next =
function(pair)
if pair.skip_next then
return { skip_next = false, value = first }
else
return { skip_next = false, value = next(pair.value) }
end
end
local finalPair = church_numeral(pred_next, pred_first)
return finalPair.value
end
return result
end
We will now develop all of the tools needed to express the above algorithm
in pure functional form, with no lua data structures or control flow.
Furthermore, we will now switch to a very ascetic style and allow
functions to have only one argument, as is the case in lambda calculus.

Church numerals are now encoded slightly differently:

Two =
function(next)
return function(first)
return next(next(first))
end
end
First, we will need functional encodings of true and false, and to
assist in reading we will create a functional encoding of "if then else".
True and false each take two arguments. True simply returns the first
argument, and False returns the second argument. "If" takes three
arguments: an encoding of a boolean value, and two expressions. It uses
the boolean value to return either the first or the second expression.

True =
 inputs:
function(arg1)
return function(arg2)
 output:
return arg1
end
end
False =
 inputs:
function(arg1)
return function(arg2)
 output:
return arg2
end
end
If =
 inputs:
function(encoded_bool)
return function(then_expression)
return function(else_expression)
 output:
return encoded_bool (
then_expression) (
else_expression)
end
end
end
> print(True(3)(4))
3
> print(False(3)(4))
4
> print(If (True) (
'the "then" expression') (
'the "else" expression'))
the "then" expression
> print(If (False) (
'the "then" expression') (
'the "else" expression'))
the "else" expression
The final tool is a small data structure, the ordered pair. Here is a
creator of ordered pairs, and a couple of functions that retrieve the
first and second elements respectively.

MakePair =
 inputs:
function(first_element)
return function(second_element)
 output:
return function(first_or_second)
return
If (first_or_second) (
first_element) (
second_element)
end
end
end
First =
function(pair)
return pair(True)
end
Second =
function(pair)
return pair(False)
end
> print(First (MakePair(3)(4)))
3
> print(Second(MakePair(3)(4)))
4
Finally, with all of the above groundwork in place, here is the lua
implementation of the predecessor function over Church numerals. Our one
remaining indulgence will be to use local variables (treated as "const"
or immutable values). We could avoid this and substitute the values
directly into the places they are used, but that would massively obfuscate
the code we are attempting to make understandable.

Pred =
 input:
function(church_numeral)
 output:
return function(next)
return function(first)
local pred_first =
MakePair (True) (first)
local pred_next =
function(pair)
return If (First(pair)) (
MakePair (False) (first)) (
MakePair (False) (next(Second(pair))))
end
local FinalPair = church_numeral (pred_next) (pred_first)
return Second(FinalPair)
end
end
end
In classic lambda calculus, we can use some shorthand names for lambda
terms such as "makepair", "true", "false", etc., and write:

λ n . λ s . λ z . second (n (λ pair . first(pair) (makepair false z) (makepair false (s (second pair))))
(makepair true z))
It is then straightforward but tedious to expand all of the shorthand
expressions above, and reduce the resulting expression to normal form.
This results in the standard magical encoding of predecessor.

[1] Cardone, Felice, and J. Roger Hindley, "History of LambdaCalculus
and Combinatory Logic",
http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf,

2006.