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, normal-form 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 zen-like in its minimality and opacity to the unenlightened.

The intent of this note is to create an on-ramp 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 non-negative 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 non-negative 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

Here is Multiply:

 
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_N-1, corresponding to the integer N-1.

The resulting function C_N-1 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 N-1 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 N-1 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

In the lua interpreter:

> 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

In the lua interpreter:

> 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 short-hand 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 short-hand 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 Lambda-Calculus and Combinatory Logic", http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf,
2006.