Notes (LCBB 03/07): The Power of Lambda

3 The Power of Lambda

3.1 Definition of Booleans

I think the pattern of using the “first” and “second” selector combinators as booleans so that you can just use the truth-condition in an “if-then-else” to directly select the right branch is really pretty.

3.2 Definition of Pairs

(M, N) = (\z. z M N)

(M, N) true = M
(M, N) false = N

Of course, an “if-then-else” is inherently a pair: a pair of two code branches that you switch between based on some condition. If you interpret the branches as data branches rather than code branches, you get a really nice representation of an ordered pair.

You can even use this pattern to construct any k-tuple. So a triple would be:

(T1, T2, T3) = (\z. z T1 T2 T3)
(T1, T2, T3) (choose-of 1 3) = T1
(T1, T2, T3) (choose-of 2 3) = T2
(T1, T2, T3) (choose-of 2 3) = T3

Where choose-of i n is an expression that gives you the i-th expression of n expressions:

choose-of 0 1 = \x1. x1    = I
choose-of 0 2 = \x1 x2. x1 = K
choose-of 1 2 = \x1 x2. x2 = K*
choose-of 0 3 = \x1 x2 x3. x1
choose-of 1 3 = \x1 x2 x3. x2
choose-of 2 3 = \x1 x2 x3. x3

How might we implement “choose of”?

Let’s start with an easier function drop which drops the first n arguments:

Well, so first lets try to build a function that adds a layer of abstraction around any expression. So for any M we want:

(\x. M) = (\ m x . m) M = K M

Which is just the K combinator. Let’s look at what happens if we apply the K combinator multiple times:

K (K M) = K (\x. M) = (\x2. (\x1 . M)) = \x2 x1. M
K (K (K M)) = K (\x2. (\x1 . M))  = (\x3. (\x2. (\x1 . M)) = \x3 x2 x1. M

We can use the exponentiation notation from the last chapter to clean this up:

K^0 M = M
K^1 M = K M
K^2 M = K (K M)

If we let M be the identity combinator, then we have our choose-n function:

drop C_m = C_m K I

drop 0  = C_0 K I = I
drop 1  = C_1 K I = K I = K*
drop 2  = C_2 K I = K (K I) = (\x y z. z)

But if there are more than n arguments:

(T1, T2, T3) (drop 1) = (C_1 K I) T1 T2 T3 = K* T1 T2 T3 = T2 T3

So our choose-of function is going to need to get rid of a bunch of arguments that come after the one we want.

Let’s define another function first n that returns the first of n + 1 arguments.

first 0 = \ x1. x1
first 1 = \ x1 x2. x1
first 2 = \ x1 x2 x3. x1

By a similar construction to drop:

first C_n = \x . C_n K x
first 0 = \x . x
first 1 = \x . K x
first 2 = \x . K (K x)

Let’s test this out:

(T1, T2, T3) (first 2) = (\x . K (K x)) T1 T2 T3
= K (K T1) T2 T3
= (K T1) T3
= T1

So our choose-of function will be:

choose-of = \ i n t. (first (sub n i)) (t (drop i))

Where sub is subtraction with Church numerals:

sub = \ x y. y pred x

pred is the predecessor or decrement function, which I explored in my notes on Tutorial Introduction to Lambda Calculus by Raul Rojas for Church numerals, and is defined below in section 3.4 for the nested pair encoding.

Honestly, this construction of n-tuples seems ugly, and I’m not the biggest fan of writing lambda expressions that are complicated enough to feel like actual code. If I’m going to write code I want some actual tools…

3.3 Definition of natural numbers as pairs

0_ = I
(n + 1)_ = (false, n_)

So numbers can be defined as nested pairs.

3.4 Lemma: Successor, predecessor, isZero

succ n_ = (n + 1)_ = (false, n_)
succ = (\n. (\p. p false n))

pred (n+1) = (\n. n false) (\p. p false n_)  = false false n_ = n_
pred = (\n. n false)

isZero = \x . x true
isZero 0 = (\x . x true) I = true
isZero 1 = (\x . x true) (\ p. p false n_) = true false n_ = false

3.5 Definition of Lambda Definability

3.6 Definition of initial functions

3.7 Definition of a class of numeric functions

A class is a collection of objects that share some property. Class A is a class of numeric functions where:

3.8 Definition of the class of recursive functions

The class of recursive functions is smallest possible class A that also has the initial functions in it.

3.9 Lemma: The initial functions are λ-definable

see 3.6.

3.10 λ closure under composition

If G, H1, .. Hm are λ-expressions, and x^ is some vector of variables, then

\ x^. G(H1 x^)... G(Hm x^)

is a lambda expression.

3.11 λ closure under primitive recursion

Basically the idea here is that we’re building a lambda expression that executes the primitive recursion calculation with a fixed-point combinator. It’s a little tedious, but looks really similar in mechanics to what I did above in 3.2 for the choose-of function.

3.12 λ closure under minimization

Again, same basic concept of using a fixed point combinator to iterate through all the natural numbers. Here we’re building an expression to return the first natural number that satisfies the predicate.

3.13 All recursive functions are λ definable

By definition, if λ-definable functions satisfy the above closures and contain the initial functions, then they are a class of recursive functions. One question this text doesn’t really cover is whether the λ-definable functions are the smallest possible class of recursive functions R. We not only need to show that all functions in R are λ-definable, but also vice-versa.

3.14 λ-definability with respect to the Church numerals

If we can convert nested pair numerals to Church numerals and back, then we can convert the above proof.

3.15 Numeral conversion

Let C_n be the n-th Church numeral, and P_n be the n-th Pair numeral:

churchToPair = \ x. x succ P_0
pairToChurch = \ x. if isZero x then C_0 else succ (pairToChurch (pred x))

3.17 Multiple Fixedpoint Theorem

Okay, so regular recursion with the fixed point theorem works like this:

Y F = X
    = F X
    = F (F X)
    = F (F (F X))
    = F (F (F (F X)))

Mutual recursion with the multiple fixed point works like this:

X1 = F1 X1 ... Xn
Xn = Fn X1 ... Xn

For n = 2:

X1 = F1 X1 X2
   = F1 (F1 X1 X2) (F2 X1 X2)
   = F1 (F1 (F1 X1 X2) (F2 X1 X2)) (F2 (F1 X1 X2) (F2 X1 X2))
X2 = F2 X1 X2
   = F2 (F1 X1 X2) (F2 X1 X2)
   = F2 (F1 (F1 X1 X2) (F2 X1 X2)) (F2 (F1 X1 X2) (F2 X1 X2))

Notice that the only difference between X1 and X2 above is outer application of F1 vs F2 and the rest of the expressions are the same.

We can collapse mutual recursion to regular recursion by constructing a new function G that has a single fixed point X:

G = \ x. [ F1 ((choose-of 1 2) x) ((choose-of 2 2) x)
         , F2 ((choose-of 1 2) x) ((choose-of 2 2) x)

where choose-of is the function that selects the k-th element of n elements in a tuple according to our construction in section 3.2. To make G more legible, lets label:

fst = choose 1 2
snd = choose 2 2

G = \ x. [ F1 (fst x) (snd x)
         , F2 (fst x) (snd x)

Now, let’s find the fixed point of G with the Y combinator from section 2.12:

Y G = X
    = G X     = [ F1 (fst X) (snd X)
                , F2 (fst X) (snd X)
    = G (G X) = [ F1 (fst (G X) (snd (G X))
                , F2 (fst (G X) (snd (G X))
              = [ F1 (F1 (fst X) (snd X)) (F2 (fst X) (snd X))
                , F2 (F1 (fst X) (snd X)) (F2 (fst X) (snd X))

It might be kinda hard to see, but this is replicating the structure of

X1 = F1 X1 X2
   = F1 (F1 X1 X2) (F2 X1 X2)
X2 = F2 X1 X2
   = F2 (F1 X1 X2) (F2 X1 X2)

in a laborious way. Watch what happens if we say:

X1 = fst X
X2 = snd X

which collapses the big complicated G (G X) expression down into:

G (G X) = [ F1 (F1 X1 X2) (F2 X1 X2)
          , F2 (F1 X1 X2) (F2 X1 X2)

In other words, X is just containing and computing our two fixed-points X1 and X2:

X = [X1, X2]

Okay, so how does this generalize to n fixed points?

X1 = F1 X1                 ... Xn
   = F1 (F1 X1 ... Xn)     ... (Fn X1 ... Xn)
   = F1 (F1 (F1 X1 ... Xn) ... (Fn X1 ... Xn))
Xn = Fn X1                 ... Xn
   = Fn (F1 X1 ... Xn)     ... (Fn X1 ... Xn)
   = Fn (F1 (F1 X1 ... Xn) ... (Fn X1 ... Xn))

We can use the same tuple construction that we did with n = 2:

X = [X1, ... , X2]
G = \ x . [ F1 ((choose-of 1 n) x) ... ((choose-of n n) x)
          , ...
          , Fn ((choose-of 1 n) x) ... ((choose-of n n) x)




ackermannGen = \ ack x y . isZero x (succ y)
                             (isZero y (ack (pred x) 1)
                               (ack (pred x) (ack x (pred y)))

ackermann = Y ackermannGen

Adapted from Andrew Black’s Church’s Lambda Calculus presentation


mGen = \ m x . isZero x ((m (succ x)) (m (pred x)))
m = Y mGen
M_n = m n


see Notes: Tutorial Introduction to Lambda Calculus by Raul Rojas, The predecessor function