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:
isZerowhich is true if the number is zero and false otherwise
succwhich 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
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 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 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 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 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
The parentheses of
@primitive must contain two things:
- the name of a “built in” function written in Swift – in this case
- 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
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.
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
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
b times. This is why the order of the parameters is reversed in the bodies of
sum, although it doesn’t matter in
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
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
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
x times and then applies that
Comparisons are relatively easy once we have observed that
diff a b is
a is less than
b and also if
b. We already have a function
isZero that will give us a boolean –
true if the argument is
false if the argument is not
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
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
gt with the body of
let isEqual = λx.λy.(geq x y) (leq x y) false let gt = λx.λy.(leq x y) false true
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.