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(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-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  > : 3 p 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) 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.
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
- have some equivalent to
else… (a conditional expression)
- Have boolean operators
Conditionals And True And False
In the Lambda Calculus, there are no traditional types, like
Bool, all we have are functions and applications, so we are going to represent
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
> 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
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
and if we have
and a b we want it to return
true if both
b are true. Or we could say, if
b else return
false. We could write that out almost verbatim using
> 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
false if you like, to verify. However, it takes seven reductions and we can do better. If
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
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
true we want to return
true no matter what
b is and if
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
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.