Lists in the Lambda Calculus

Some Lambda Calculator Enhancements

In version 1.2.1 of the Lambda Calculator, I have added the concept of a meta command. A meta command starts with a / (forward slash) and is used for doing things outside of the Lambda Calculus (forward slash is sort of the opposite of backslash, which is my alternate way of entering a λ. I have two meta commands so far:

• /listDefs
• /read

Rather than go into detail about what they do, here’s an example.

jeremyp@eleanor LambdaCalculus % swift run
> /listDefs
: 0 defnitions:

> /read definitions.txt
: defined cond as λp.λa.λb.p a b
: defined true as λx.λy.x
: defined false as λx.λy.y
: defined not as λa.a false true
: defined and as λa.λb.a b false
: defined or as λa.λb.a true b
: defined equals as λa.λb.a b (b false true)
> /listDefs
: 7 defnitions:
let cond = λp.λa.λb.p a b
let true = λx.λy.x
let false = λx.λy.y
let not = λa.a false true
let and = λa.λb.a b false
let or = λa.λb.a true b
let equals = λa.λb.a b (b false true)

definitions.txt is a file that’s included in the git rep for the Lambda Calculator. This is it at the time of writing.

let cond = (λp.λa.λb.p a b)

let true = (λx.λy.x)
let false = (λx.λy.y)

let not = λa.a false true
let and = λa.λb.a b false
let or = λa.λb.a true b
let equals = λa.λb.a b (b false true)

#reverseInto = λl1.λl2.if (isEmpty l1) then l2 else (reverseInto (tail l1) (cons (head l1) l2))
#reverseInto' = (λf.λl1.λl2.if (isEmpty l1) then l2 else (f (tail l1) (cons (head l1) l2))) reverseInto'
#             = (λf.λl1.λl2.cond (isEmpty l1) l2 (f (tail l1) (cons (head l1) l2))) reverseInto'

/read reads a file and uses it for input into the REPL. You can see from the file (and the example above) that there is one new feature which is that lines beginning with # (hash) are ignored. This gives us the ability to add comments to our files.

With that out of the way, let’s talk about lists. As per my previous post, most of this material comes from another article I found on the web: Lambda Calculus(part II).

Lists

Lists are flexible data structures that are beloved of functional programming languages, probably because they are really easy to manipulate with recursion. For our purposes, a list is either empty or it is an ordered pair of objects (h, t), the first of which is the first item or “head” of the list and the second of which (or “tail”) is a list consisting of all the other items on the list. If we have a list of fruits: apple, pear, banana, it’s represented by the ordered pair (apple, list-of-pear-and-banana). list-of-pear-and-banana is itself represented by an ordered pair (pear, list-of-banana) and list-of-banana is represented by an ordered pair: (banana, empty-list). empty-list is a list with no objects in it, which we call nil. Conceptually, this is what our list looks like:

(apple, (pear, (banana, nil)))

How do we represent lists in the Lambda Calculus? We’ll start by examining ordered pairs. How do we represent ordered pairs? Well, let’s think about the operations we might want to perform with ordered pairs.

• Given two arbitrary expressions a and b, we need to be able to construct an ordered pair p from them
• Given an ordered pair p we need to be able to extract the first element a from it
• Given an ordered pair p we need to be able to extract the second element b from it

Ignoring construction for now, if we have an ordered pair (a, b) we can extract the first element with something like: (λx.λy.x) a b and the second with something like (λx.λy.y) a b. In both cases, we have a function applied to a air of arguments. If we abstract the function, we have our implementation of an ordered pair i.e. λf.f a b. In English, an ordered pair is a function that applies its argument (that must also be a function) to a pair of expressions.

You will have observed that the function I used above to get the first element λx.λy.x is the same as our definition of true and the function to get the second element is the same as our definition of false. So, to satisfy the second two bullet points above, we could just say “use p true and p false respectively”. However, this is a bit objected oriented, and that’s out of favour right now. We want a function that takes the pair as an argument. Fortunately, that’s easily done by abstracting out the pair e.g.λp.p true to get the first element and λp.p false to get the second element.

How do we construct an ordered pair? Well, we need a function that takes two arguments a and b and reduces to λf.f a b. That’s pretty simple, we can just abstract a and b from λf.f a b to get λa.λb.λf.f a b.

That’s ordered pairs dealt with. Now, let’s look at lists. What kinds of operations do we want to perform on lists.

• Given an arbitrary expression h and a list t, we need to be able to construct another list l from them
• Given a non empty list l we need to be able to extract the head element h from it
• Given a non empty list l we need to be able to extract the tail t from it
• Given a list l we need to be able to determine if it is empty.

Since a non empty list is an ordered pair, the first three operations are identical to the first three operations for ordered pairs. cons, head and tail are defined as follows:

let cons = λh.λt.λf.f h t
let tail = λl.l (λx.λy.y)
let head = λl.l (λx.λy.x)

Let’s try these out. Firstly, cons.

> cons banana nil
: (λh.λt.λf.f h t) banana nil
> 
: (λt.λf.f banana t) nil
> 
: λf.f banana nil
> let l1 = λf.f banana nil

Here I have constructed a list of one element: “banana”. Note that nil is not defined yet, it’s just an arbitrary variable. I have given the constructed list a name to make it easier to build more lists using it.

> cons pear l1
: (λh.λt.λf.f h t) pear (λf.f banana nil)
> 
: (λt.λf.f pear t) (λf.f banana nil)
> 
: λf.f pear (λf.f banana nil)
> let l2 = λf.f pear (λf.f banana nil)

Now I have a two element list.

> cons apple l2
: (λh.λt.λf.f h t) apple (λf.f pear (λf.f banana nil))
> 
: (λt.λf.f apple t) (λf.f pear (λf.f banana nil))
> 
: λf.f apple (λf.f pear (λf.f banana nil))
> let l3 = λf.f apple (λf.f pear (λf.f banana nil))

And now a three element list.

> cons l2 l3
: (λh.λt.λf.f h t) (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil)))
> 
: (λt.λf.f (λf.f pear (λf.f banana nil)) t) (λf.f apple (λf.f pear (λf.f banana nil)))
> 
: λf.f (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil)))
> let l4 =  λf.f (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil)))

This is a four element list whose first element is itself a list.

> head l3
: (λl.l (λx.λy.x)) (λf.f apple (λf.f pear (λf.f banana nil)))
> 
: (λf.f apple (λf.f pear (λf.f banana nil))) (λx.λy.x)
> 
: (λx.λy.x) apple (λf.f pear (λf.f banana nil))
> 
: (λy.apple) (λf.f pear (λf.f banana nil))
> 
: apple

This gets the first item in l3. As we hoped, it reduces to apple.

> tail l2
: (λl.l (λx.λy.y)) (λf.f pear (λf.f banana nil))
> 
: (λf.f pear (λf.f banana nil)) (λx.λy.y)
> 
: (λx.λy.y) pear (λf.f banana nil)
> 
: (λy.y) (λf.f banana nil)
> 
: λf.f banana nil

And this gets us the tail of l2 which is the same as the list l1.

IsEmpty And the Definition of Nil

isEmpty needs to be a function such that, for any non empty list l,

isEmpty l →_β false

isEmpty nil →_β true

(The notation →_β means “β reduces to”.)

Let’s take th case of a non empty list first. A non empty list is a function of the form λf.f h t. So what we need is an argument for the list (call it isEmpty') that β reduces it to false. i.e.

(λf.f h t) isEmpty' →_β false

If we do one reduction, we get isEmpty' h t, so isEmpty' needs to be a function of two arguments that always returns false. That’s easy enough: it’s λh.λt.false. Let us try it with a non empty list.

> l4 (\h.\t.false)
: (λf.f (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil)))) (λh.λt.λx.λy.y)
> 
: (λh.λt.λx.λy.y) (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil)))
> 
: (λt.λx.λy.y) (λf.f apple (λf.f pear (λf.f banana nil)))
> 
: λx.λy.y

All we need to do now is abstract the list so we get a function that takes a list as an argument rather than a list that takes a function as an argument.

> let isEmpty = λl.l (λh.λt.false)
: defined isEmpty as λl.l (λh.λt.false)
> isEmpty l4
: (λl.l (λh.λt.λx.λy.y)) (λf.f (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil))))
> 
: (λf.f (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil)))) (λh.λt.λx.λy.y)
> 
: (λh.λt.λx.λy.y) (λf.f pear (λf.f banana nil)) (λf.f apple (λf.f pear (λf.f banana nil)))
> 
: (λt.λx.λy.y) (λf.f apple (λf.f pear (λf.f banana nil)))
> 
: λx.λy.y

It works! All we need now is a definition of nil that returns true instead of false. If we do one reduction of isEmpty nil we get nil (λh.λt.λx.λy.y) and we want

nil (λh.λt.λx.λy.y) →_β true

nil therefore has to be a function that ignores its argument and returns true. nil should be λf.true

> let nil = \f.true
: defined nil as λf.true
  cleared current expression
> isEmpty nil
: (λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x)
> 
: (λf.λx.λy.x) (λh.λt.λx.λy.y)
> 
: λx.λy.x

Now we have all the tools we need to manipulate lists, except for one thing: lists may be of arbitrary length. So, how would we get the last item in a list. For example, in l3 (which is λf.f apple (λf.f pear (λf.f banana nil))), how would we get “banana”. In this case, we can do

> head (tail (tail l3))
: (λl.l (λx.λy.x)) ((λl.l (λx.λy.y)) ((λl.l (λx.λy.y)) (λf.f apple (λf.f pear (λf.f banana nil)))))
> 
: (λl.l (λx.λy.y)) ((λl.l (λx.λy.y)) (λf.f apple (λf.f pear (λf.f banana nil)))) (λx.λy.x)
> 
: (λl.l (λx.λy.y)) (λf.f apple (λf.f pear (λf.f banana nil))) (λx.λy.y) (λx.λy.x)
> 
: (λf.f apple (λf.f pear (λf.f banana nil))) (λx.λy.y) (λx.λy.y) (λx.λy.x)
> 
: (λx.λy.y) apple (λf.f pear (λf.f banana nil)) (λx.λy.y) (λx.λy.x)
> 
: (λy.y) (λf.f pear (λf.f banana nil)) (λx.λy.y) (λx.λy.x)
> 
: (λf.f pear (λf.f banana nil)) (λx.λy.y) (λx.λy.x)
> 
: (λx.λy.y) pear (λf.f banana nil) (λx.λy.x)
> 
: (λy.y) (λf.f banana nil) (λx.λy.x)
> 
: (λf.f banana nil) (λx.λy.x)
> 
: (λx.λy.x) banana nil
> 
: (λy.banana) nil
> 
: banana

Unfortunately, that doesn’t get the last element, it gets the third element which happens to be the last element of l3 by coincidence. We need recursion. For any non empty list, the last element is either:

1. the head of the list, if the tail is empty
2. the last element of the tail of the list.

A naive implementation would look something like:

let naiveLast = λl.(isEmpty (tail l)) (head l) (naiveLast (tail l))

Let’s try it with l1 which represents the case where tail l is nil.

> let naiveLast = λl.(isEmpty (tail l)) (head l) (naiveLast (tail l))
: defined naiveLast as λl.isEmpty (tail l) (head l) (naiveLast (tail l))
> naiveLast l1
: (λl.(λl.l (λh.λt.λx.λy.y)) ((λl.l (λx.λy.y)) l) ((λl.l (λx.λy.x)) l) (naiveLast ((λl.l (λx.λy.y)) l))) (λf.f banana (λf.λx.λy.x))
> 
: (λl.l (λh.λt.λx.λy.y)) ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) ((λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x)) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λf.f banana (λf.λx.λy.x)) (λx.λy.y) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λx.λy.y) banana (λf.λx.λy.x) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λy.y) (λf.λx.λy.x) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λf.λx.λy.x) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λx.λy.x) ((λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λy.(λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))) (naiveLast ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))))
> 
: (λl.l (λx.λy.x)) (λf.f banana (λf.λx.λy.x))
> 
: (λf.f banana (λf.λx.λy.x)) (λx.λy.x)
> 
: (λx.λy.x) banana (λf.λx.λy.x)
> 
: (λy.banana) (λf.λx.λy.x)
> 
: banana

Now, let’s try it with l2 which should take us down the recursive case.

> naiveLast l2
: (λl.(λl.l (λh.λt.λx.λy.y)) ((λl.l (λx.λy.y)) l) ((λl.l (λx.λy.x)) l) (naiveLast ((λl.l (λx.λy.y)) l))) (λf.f pear (λf.f banana (λf.λx.λy.x)))
> 
: (λl.l (λh.λt.λx.λy.y)) ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x))) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λf.f pear (λf.f banana (λf.λx.λy.x))) (λx.λy.y) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λx.λy.y) pear (λf.f banana (λf.λx.λy.x)) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λy.y) (λf.f banana (λf.λx.λy.x)) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λf.f banana (λf.λx.λy.x)) (λh.λt.λx.λy.y) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λh.λt.λx.λy.y) banana (λf.λx.λy.x) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λt.λx.λy.y) (λf.λx.λy.x) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λx.λy.y) ((λl.l (λx.λy.x)) (λf.f pear (λf.f banana (λf.λx.λy.x)))) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: (λy.y) (naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x)))))
> 
: naiveLast ((λl.l (λx.λy.y)) (λf.f pear (λf.f banana (λf.λx.λy.x))))
> 
: naiveLast ((λf.f pear (λf.f banana (λf.λx.λy.x))) (λx.λy.y))
> 
: naiveLast ((λx.λy.y) pear (λf.f banana (λf.λx.λy.x)))
> 
: naiveLast ((λy.y) (λf.f banana (λf.λx.λy.x)))
> 
: naiveLast (λf.f banana (λf.λx.λy.x))

We got as far as reducing it to the equivalent of the l1 case. Unfortunately, we can’t go any further because this naiveLast is not the same naiveLast of the definition. It was unbound in naiveLasts definition. We can’t do recursion directly in the Lambda Calculus. How we get around this problem is the topic of discussion in the next post.