The Other Day in Prof Dan Friedman S Advanced Programming Languages Class We Had an Assignment

Some context –

The other day in Prof Dan Friedman’s Advanced Programming Languages class we had an assignment where we had to write a lambda calculus interpreter that did non deterministic application and we had to write the factorial in it. Also, reduction was to continue even if the top level term was value.

As a consequence of working on this we were expected to discover a method of encoding numbers using pure lambda terms. A really long time back AlonzoChurch (creator of the lambda calculus) created an encoding now called the Church numerals. I created the following set when working on the factorial problem.

t = \a.\b.a true

f = \a.\b.b false

zero = \x.t

zero? = \x.(x f)

s = \x.\b.((b x) b) successor

p = \x.(x t) predecessor

(Like in Haskell the ‘\’ represent lambda). So we have a way of saying zero, we have a way of checking if a number is zero and we have the ability to add one and subtract one. That gives us all the natural numbers including zero.

If you notice, the predecessor define above returns a value that is an invalid number when applied to zero. An alternate ‘type safe’ definition is the following –

p = \x.(((zero? x) x) (x t))

Here (p zero) is zero.

Now you may think that that’s not great way of implementing numbers – its inefficient etc. Yes that’s true, but remember that the lambda calculus is a formal system, it’s a mathematical formalism and hence has no notion of cost. In the study of formal systems (other than the study of their complexity) we are interested in asking questions about what the system can do and cannot do. The above encoding I believe is equivalent to the encoding of Church numerals.

Following the definition of numbers, I can define ‘add’ in the following obvious way -

add = (Y \add.\a.\b.(((zero? a) b) ((add (p a)) (s b)))

Here ‘Y‘ is the fixed point Y combinator and this is equivalent to

add(a, b) { if a == 0 then return b else return add(a - 1, b + 1) }

Similarly one can define ‘mul’ and ‘factorial’ as well.

I went ahead and defined operators so that I have scheme/lisp style lists. I am told that there are very similar to Church’s definitions.

cons = \x.\y.\b1.\b2.((b1 f) ((b2 x) y))

car = \ls.((ls #f) #t)

cdr = \ls.((ls #f) #f)

null = \x.x

null? = \ls.(ls #t)

Hence we have –

(null? null) -> #t

(car null) -> undefined

(cdr null) -> undefined

(car (cons a b)) -> a

(cdr (cons a b)) -> b

Can you shoot yourself in the foot using these definitions? Of course you can – but if you are careful you can write meaningful programs as well. To do other sorts of checks, like to prevent us from doing (s cons) we need some kind of type system or validations rules – but these are not relevant to the discussion of the pure lambda calculus.

Here is a basic lambda calculus reference -

Here is a Church encoding reference -

Roshan James

Sunday, February 19, 2006