## Recap

In the last post not dealing with the internals of the Lambda Calculator, we introduced Church Numerals and some basic operations. There are actually only two operations that are needed and these are:

`isZero`

which is true if the number is zero and false otherwise`succ`

which gives us the successor of any Church numeral – i.e. the number plus one.

We further defined `pred`

in terms of `succ`

and some other functions in Lambda Calculus and we touched on how to define addition, multiplication and subtraction in terms of `succ`

and `pred`

.

## Changes to Lambda Calculator

To make the following discussions a little easier to follow and make the examples a bit more tractable, I’ve made some enhancements to the Lambda Calculator. These are discussed briefly below. These features are all available in version 3.2.0. All are optional which means when you first fire up the Lambda Calculator, you are in “vanilla” mode and you have to enable them.

### Continuous Mode

Continuous mode is currently enabled with the meta command `/toggleContinuous`

. In this mode, the calculator does not just do one beta reduction: it performs beta reductions in a loop until there are no more to be done. This means that you don’t have to press `return` hundreds of times to reduce an expression to its normal form. On the down side, you also don’t see the intermediate steps of a reduction.

### Numerals

Numerals are syntactic sugar for Church Numerals. When you enable them with `/toggleNumerals`

, the parser will parse anything that looks like a positive whole number as a special abstraction called a `Numeral`

. A `Numeral`

behaves exactly as if it was an abstraction of the form `λf.λx.f .... (f x)..)`

except that when printing, it prints as the number it represents.

### Primitives

Primitives are an attempt to speed up the Lambda Calculator by short cutting some operations and also to preserve numerals. For example

```
> succ 1
: λf.λx.f (f x)
```

Is technically correct, but it would be nice if we had

```
> succ 1
: 2
```

Also, it takes four beta reductions to calculate the successor of a number. Primitives provide native Swift hooks for certain definitions. For example, there is a primitive for `succ`

defined as follows:

`let succ = @primitive(numeralSuccessor λn.λf.λx.n f (f x))`

`@primitive( ... )`

denotes a primitive. The `@`

denotes an annotation which fills a similar role to annotations in languages like Java and Swift. There’s only one annotation available so far and that’s `@primitive`

.

The parentheses of `@primitive`

must contain two things:

- the name of a “built in” function written in Swift – in this case
`numeralSuccessor`

- an alternate expression which must be an abstraction.

The alternate is used if the built in function can’t handle the argument passed to it. For example, `numeralSuccessor`

can calculate the successor to a `Numeral`

but it doesn’t know how to handle anything else as an argument: `succ banana`

is perfectly legal in the Lambda Calculus but doesn’t reduce to a numeral. If a non-numeral is passed in, it falls back to the alternate and reduces it normally.

Primitives are not a wholly successful addition to the Lambda Calculator. For example, I was hoping that `succ (pred 2)`

would reduce to 2 but it actually reduces to `λf.λx.f (f x)`

which is correct but not 2. The problem is that the first beta reduction substitutes the argument `pred 2`

into the `succ`

. `pred 2`

beta reduces to a numeral but it is not itself a numeral and so the alternate expression is used instead of the primitive.

## Arithmetic

In the examples, I’ll be using the new “continuous mode” of Lambda Calculator. In continuous mode, instead of stopping after each beta reduction, the calculator keeps going until there are no more beta reductions to do – or forever if the computation is infinite.

Let’s start with addition. The sum of two numbers can be defined as

`let sum = λx.λy.y succ x`

This is pretty simple. It just applies `succ`

to `x`

`y`

times. Since addition is commutative, we could also have defined it as `λx.λy.x succ y`

but I wanted to keep it consistent with subtraction. Subtraction is defined very similarly.

`let diff = λx.λy.y pred x`

`diff a b`

calculates `a - b`

. By starting at `a`

and applying the `pred`

function `b`

times. This is why the order of the parameters is reversed in the bodies of `diff`

and `sum`

, although it doesn’t matter in `sum`

.

If the first argument is smaller than the second, the difference will be zero. We don’t have any negative numbers, so there is no defined answer for subtracting a larger number from a smaller one. We should probably loop forever, but having the answer come out to `0`

is advantageous for defining comparison operations.

```
> diff 4 6
: 0
```

Note that, in terms of efficiency, this seemingly innocuous definition lacks it in the extreme. For each use of `pred`

we count up from zero to the number for which we want the predecessor. We have to do that `y`

times. For example, to get the difference between `5`

and `4`

, we first need the predecessor of `5`

which takes five applications of `succ`

, then the predecessor of `4`

(four applications of `succ`

) then the predecessor of `3`

(three applications of `succ`

), then the predecessor of `2`

(two applications of `succ`

). This is a total of fourteen applications of `succ`

. The relationship of argument magnitude to speed is essentially quadratic.

Multiplication is also pretty easy. `prod a b`

is adding `b`

to `0`

`a`

times. We could define it thus

```
> let prod = λx.λy.y (sum x) 0
> prod 5 4
: λf.λx.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))
```

The definition I chose for Lambda Calculator, however, is

`let prod = λx.λy.y (x succ) 0`

This is the same as the previous definition but is slightly optimised by beta reducing `sum x`

. It creates a function that applies the `succ`

function `x`

times and then applies *that* `y`

times.

## Comparisons

Comparisons are relatively easy once we have observed that `diff a b`

is `0`

if `a`

is less than `b`

and also if `a`

equals `b`

. We already have a function `isZero`

that will give us a boolean – `true`

if the argument is `0`

and `false`

if the argument is not `0`

.

```
let leq = λx.λy.isZero (diff x y)
> leq 5 4
: false
> leq 4 4
: true
> leq 4 5
: true
>
```

`geq`

is defined simply by reversing the order of the parameters in the body of the function.

If one number is strictly greater than another number, it is obviously not less than or equal to it. This gives us the definition of “greater than”.

```
let gt = λx.λy.not (leq x y)
> gt 5 4
: true
> gt 4 4
: false
> gt 4 5
: false
```

`lt`

is defined similarly but built on `geq`

.

That only leaves equality. Two numbers are equal if they are both less than or equal to each other or both greater than or equal to each other. `isEqual`

can therefore be defined as

```
let isEqual = λx.λy.and (geq x y) (leq x y)
> isEqual 5 4
: false
> isEqual 4 4
: true
> isEqual 4 5
: false
```

There is an optimised version though that effectively beta reduces the application of `and`

. We can use the body of `and`

directly. Similar things can be done for `lt`

and `gt`

with the body of `not`

.

```
let isEqual = λx.λy.(geq x y) (leq x y) false
let gt = λx.λy.(leq x y) false true
```

## Conclusion

Now we have the tools to do basic arithmetic and comparisons. You may have noticed that I’m still avoiding division. The reason for this is, of course that it is complicated. However, there is a lot we can do just with what we have so far and we’ll discuss some of this in a future blog post.