The Magic of Lambda

Rediscovering the magic of the Lambda calculus ¹ has been one of the pleasures that the gift of time the mid-winter holiday delivered this year 2020. It really is a remarkable thing to realise that the whole of the (classical ²) computational substrate can be realised in such a simple and elegeant formalism.

Resorting to bare bones Haskell I followed along in the clear and rigorous exposition in Types and Programming Languages by Benjamin C. Pierce and completed the exercises as I went.

Of course not all the terms are very useful for real world programming, indeed Church numerals are quite inefficient in this form but the remarkable thing is how they can be expressed at all and how we can derive all the equipment we would expect for complex (Turing complete) computation.

Here is a taste of the first few untyped Lambda calculus combinators re-expressed in what is, trivially, Haskell. Notice that I use curried forms (single argument) lambda forms here as this is what Haskell is doing under the sugar as all its functions are curried.

I’ll be continuing with this exploration into the simply typed variety and beyond into the far reaches of the The Lambda Cube

Church booleans

\(\lambda t. \lambda f.\: t\)

tru = \t -> \f -> t

\(\lambda t. \lambda f.\: f\)

fls = \t -> \f -> f

\(\lambda b. \lambda b.\: b\: c\: fls\)

and = \b -> \c -> b c fls

\(\lambda b. \lambda c.\: b\: tru\: c\)

or = \b -> \c -> b tru c

\(\lambda b.\: b\: fls\: tru\)

not = \b -> b fls tru

Pairs

pair = \f -> \s -> \b -> b f s

fst = \b -> b tru

snd = \b -> b fls

Church numerals

zero - interestingly c0 is a pun of fls

c0 = \s -> \z -> z

c1 = \s -> \z -> s z

c2 = \s -> \z -> s (s z)

c3 = \s -> \z -> s (s (s z))

etc.

Sucessor to a Church numeral can be defined

scc = \n -> \s -> \z -> s (n s z)

alternatively

scc1 = \n -> \s -> \z -> n (s (s z))

c4 = scc c3

c5 = scc c4

etc.

Addition of two Church numerals works by applying s n times to z and then applies s iterated m more times to the result

plus = \m -> \n -> \s -> \z -> m s (n s z)

Add together m copies of n

times = \m -> \n -> m (plus n) c0

without plus: apply n sucessors to z m times

times2 = \m -> \n -> \s -> \z -> m (n s) z

eta reduced

times3 = \m -> \n -> \s -> m (n s)

exponentiation

power = \m -> \n -> m (times n) c1

power2 = \m -> \n -> m n

zero predicate

iszro = \m -> m (\_ -> fls) tru

subtraction is a lot more tricky

zz = pair c0 c1

ss = \p -> pair (snd p) (plus c1 (snd p))

and requires a predecessor term

prd = \m -> fst (m ss zz)

sub = \m -> \n -> n (prd m)

equality of Church numerals

eql = \m -> \n -> iszro (n sub m)