Higher Level Concepts In The Lambda Calculus

Some Syntactic Sugar

We are going to be talking about some pretty high level concepts in this post, like true and false and maybe even the natural numbers (although that might be too high level and need to be left to the next post). You’ve probably realised that the Lambda Calculus has no means of naming things and everything has to be written out in full. This will get tedious very quickly and also hard to understand. For example:

 λn.(λp.λa.λb.p a b) n (λx.λy.y) (λx.λy.x)

What is that? It’s actually one way of defining the concept of boolean negation, which is to say that it is the function not where not(true) = false and not(false) = true.

Fortunately, in version 1.1 of the lambda calculator, I have created some syntactic sugar so we can write not in a more human friendly way. Let me introduce you to let. A let statement is of the form:

let <variable> = <lambda-expression>

For example, if I have a lambda expression λx.λy.x p y that I want to use in lots of places, I can write a let expression:

let plus = λx.λy.x p y

Now I can use plus in place of λx.λy.x p y.

> let plus = λx.λy.x p y
: defined plus as λx.λy.x p y
> plus 3 2
: (λx.λy.x p y) 3 2
> 
: (λy.3 p y) 2
> 
: 3 p 2
> plus 3 (plus 2 4)
: (λx.λy.x p y) 3 ((λx.λy.x p y) 2 4)
> 
: (λy.3 p y) ((λx.λy.x p y) 2 4)
> 
: 3 p ((λx.λy.x p y) 2 4)
> 
: 3 p ((λy.2 p y) 4)
> 
: 3 p (2 p 4)

You’ll notice that, after using plus in a lambda expression, the calculator immediately substitutes it for its lambda expression. It’s important to realise that let expressions do not add any new power or features to the language. In particular, it does not allow us to sneak recursion into the Lambda Calculus. For example:

> let recurse = \x.x recurse
: defined recurse as λx.x recurse
  cleared current expression
> recurse 1
: (λx.x recurse) 1
> 
: 1 recurse
> 
: 1 recurse
> 

The reason for this is that the let syntax is actually just syntactic sugar for an application of an abstraction to the expression part of the let. So, if we have typed in let name = name-expression, any further expression we type in (call it some-expression) will be wrapped as follows:

(λname.some-expression) name-expression

Instances of name in name-expression are free, which is why, in the example above, recurse is never reduced.

NB: the phrase  “cleared current expression” that appears after the response to the let occurs because I had been evaluating an expression and the calculator has now thrown it away.

Note To the Reader

As with my previous post, I have based most of the material in the rest of this post on another web page. In this case it’s Lambda Calculus (Part II).

Also, if you take the time to read the linked article, you’ll see it starts by talking about Currying. All functions in the Lambda Calculus take one argument but Currying is a mechanism which shows how you get multi-argment functions for free. Looking at the PLUS example above for a moment:

> let plus = λx.λy.x p y
: defined plus as λx.λy.x p y
> plus 3 2
: (λx.λy.x p y) 3 2
> 
: (λy.3 p y) 2            [1]
> 
: 3 p 2                   [2]

PLUS looks like a function that takes two arguments, but actually, it is a function that takes one argument and returns a new function (see[1]) that “adds” PLUS‘s argument to whatever follows. I’m mentioning this now, because, in the rest of this post, I’m going to be talking about functions of two and three arguments and perhaps more. When I say “this function takes two arguments” what I really mean is “this function takes one argument and returns another function that takes one argument. When I say “this function takes three arguments” I really mean “this function takes one argument that returns another function that takes one argument and this second function returns a third function that takes one argument.

Booleans

Let’s start with the easy stuff. How do we define true and false and the operations we can do to them. What sort of things do we need to do:

• represent the values true and false.
• have some equivalent to if … then … else … (a conditional expression)
• Have boolean operators and, or, not.

Conditionals And True And False

In the Lambda Calculus, there are no traditional types, like Int or Bool, all we have are functions and applications, so we are going to represent true and false by functions. Which functions we use will become apparent when we define our conditional expression.

A conditional has three arguments: the first is a boolean expression; the second is the expression returned when the boolean evaluates to true; the third is the expression returned when the boolean evaluates to false. In some languages you would write if p then a else b but we don’t have infix syntax, so we instead write cond p a b. “Cond” is short for “conditional” and it comes from Lisp. What is cond? It’s this: (λp.λa.λb.p a b). Let’s try it but without defining what true and false are.

> let cond = (λp.λa.λb.p a b)
: defined cond as λp.λa.λb.p a b
> cond true M N
: (λp.λa.λb.p a b) true M N
> 
: (λa.λb.true a b) M N
> 
: (λb.true M b) N
> 
: true M N

At this point we can’t go any further because true is a free variable. If we had used false instead, we would have ended up with false M N. Hopefully, it should be clear that true should be a function that selects the first of two arguments and false should be a function that selects the second of two arguments. If this is the case, true M N will reduce to M and false M N will reduce to N as required. Let’s try it.

> let cond = (λp.λa.λb.p a b)
: defined cond as λp.λa.λb.p a b
> let true = \x.\y.x
: defined true as λx.λy.x
> let false = \x.\y.y
: defined false as λx.λy.y
> cond true M N
: (λp.λa.λb.p a b) (λx.λy.x) M N
> 
: (λa.λb.(λx.λy.x) a b) M N
> 
: (λb.(λx.λy.x) M b) N
> 
: (λx.λy.x) M N
> 
: (λy.M) N
> 
: M
> cond false M N
: (λp.λa.λb.p a b) (λx.λy.y) M N
> 
: (λa.λb.(λx.λy.y) a b) M N
> 
: (λb.(λx.λy.y) M b) N
> 
: (λx.λy.y) M N
> 
: (λy.y) N
> 
: N

And And OR

Starting with and if we have and a b we want it to return true if both a and b are true. Or we could say, if a is true return b else return false. We could write that out almost verbatim using cond.

> let and1 = \a.\b.cond a b false
: defined and1 as λa.λb.cond a b false
  cleared current expression
> and1
: λa.λb.(λp.λa.λb.p a b) a b (λx.λy.y)

That’s quite complicated, but it does work.

> and1 true false
: (λa.λb.(λp.λa.λb.p a b) a b (λx.λy.y)) (λx.λy.x) (λx.λy.y)
> 
: (λb.(λp.λa.λb.p a b) (λx.λy.x) b (λx.λy.y)) (λx.λy.y)
> 
: (λp.λa.λb.p a b) (λx.λy.x) (λx.λy.y) (λx.λy.y)
> 
: (λa.λb.(λx.λy.x) a b) (λx.λy.y) (λx.λy.y)
> 
: (λb.(λx.λy.x) (λx.λy.y) b) (λx.λy.y)
> 
: (λx.λy.x) (λx.λy.y) (λx.λy.y)
> 
: (λy.λx.λy.y) (λx.λy.y)
> 
: λx.λy.y

The last line you should recognise is what false is defined as. You can try it with the other combinations of true and false if you like, to verify. However, it takes seven reductions and we can do better. If a is true it is a function that selects its first argument, so, if we can make and true b reduce to λb.true b _ (I use _ to denote we don’t care what the second argument is, because true throws it away), we would get the right answer. Similarly, if a is false, it selects its second argument and we want it to return false so if we can make and false b reduce to λb.false _ false, we will also get the right answer. Well that’s easy, replace the _ in the first expression with false and the _ in the second expression with b and we get:

λb.true b false and λb.false b false

Abstract out the first term in each case as a and we get

λa.λb.a b false.

Let’s try it.

> let and = λa.λb.a b false
: defined and as λa.λb.a b false
  cleared current expression
> and true false
: (λa.λb.a b (λx.λy.y)) (λx.λy.x) (λx.λy.y)
> 
: (λb.(λx.λy.x) b (λx.λy.y)) (λx.λy.y)
> 
: (λx.λy.x) (λx.λy.y) (λx.λy.y)
> 
: (λy.λx.λy.y) (λx.λy.y)
> 
: λx.λy.y

The last line is the definition of false as required. It works for all the other combinations of true and false but I’ll leave confirming that as an exercise for the reader.

Similar reasoning can be used to arrive at a definition of or. In this case, if a is true we want to return true no matter what b is and if a is false we want to return whatever b is. Thus, we have or = λa.λb.a true b

> let or = \a.\b.a true b
: defined or as λa.λb.a true b
  cleared current expression
> or true false
: (λa.λb.a (λx.λy.x) b) (λx.λy.x) (λx.λy.y)
> 
: (λb.(λx.λy.x) (λx.λy.x) b) (λx.λy.y)
> 
: (λx.λy.x) (λx.λy.x) (λx.λy.y)
> 
: (λy.λx.λy.x) (λx.λy.y)
> 
: λx.λy.x

not is also easily defined as λa.a false true. equals is defined as λa.λb.a b (b false true) which says “if a is true return b, if a is false return not b. By symmetry, xor is defined as λa.λb.a (b false true) b

That’s booleans sorted. The next subject will be lists but I want to make some more improvements to the lambda calculator first, to make our lives easier.