Church Encoded Numbers with Lambda Calculus

05-Jan-2014 06:55AM

So the saga of Programming with Patterns continues, this time with Lambda calculus. Here are the things worth knowing about Lambda Calculus for laymen like myself.

Lambda Calculus is an equivalent of Turing Machines in its computational ability. Unlike Turing Machines, rather than dealing with operations on state, Lambda Calculus is composed purely of functions, specifically lambda functions. These are pure functions with no side affects, and as you can observe, the universe seems composed purely of the side affects of phenomena. Despite this, just like in typical mathematics, we can create abstractions that simulate the universe and ideas to perform the computation of our desires!

In our lesson with Barry Jay on Lambda Calculus, we were exposed to Church Encoding, an equivalent of Natural Numbers. Wikipedia will do a better job of explaining the theory than I ever could, but below I give an example of these implemented in the Pattern Calculus language bondi, using different variable names to our lecturer for clear and intuitive understanding.

( Remember that things in these parens are comments)

(* The aim here is to create numbers that can be used as:
 ~~three increment 0;;
> 3
~~ (add four five) increment 0;;
> 9

let zero = fun f -> fun x -> x;;
(*Zero is equivalent to:
Number zero (Function increment, Number startingNum) {
     return startingNum;

let successor = fun n -> fun f -> fun x -> n f (f x);;
Let successor = (lambda (Function zeroOrSuccessor) { 
                               lambda (Function increment) { 
                                         Number (Function startingNum) {
                                                   return zeroOrSuccessor(increment, increment( startingNum ) );

So what happens is that every layer of successor increments "startingNum" until it reaches the zero function and startingNum is returned.

let one = successor zero;;
let two = successor one;;
let three = successor two;;
let four = successor three;;
let five = successor four;;
let six = successor five;;
(*These numbers can be seen as:
 three ~= (successor (successor (successor zero)))
and can be evaluated with (three inc 0) 

(* Typical increment function. *)
let increment = fun x -> x + 1;;

let plus = fun x -> fun y -> ((x successor) y);;
let expt = fun x -> fun y -> (y x)
let mul = fun x -> fun y -> (x (y successor) zero);;

But why does this matter?

The following is conjecture, and should only be taken with a grain of salt. Obviously, a computer that implements Church Encoding is slower than the typical bit manipulation, but what it does show is that Lambda Calculus can produce an abstraction that is functionally identical to Natural Numbers represented with bits. As with anything equivalent, they can be swapped out without impact to their universe, so long as Types are used to enforce that the swapped out abstractions aren't used invalidly. Because of that, we can enjoy both the power and expressiveness of completely functional language without sacrificing the speed advantages of our modern computer chips.