# 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.

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.

## 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.

This site uses Akismet to reduce spam. Learn how your comment data is processed.