Lambda Calculus: More Numbers

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.