Lambda Calculus: Subtraction is hard

In the last article I defined the Succ operation on numbers and showed how this can be used to implement addition in untyped lambda calculus.

Because of the number representation I choose this was rather easy so Subtraction should be not that hard right?

Well … wrong.

You might want to stop here and try to define a Pred operation yourself that takes a number and returns the predecessor (-1) of that number or zero if there is none (because 0 is not the successor of any natural number there should be no predecessor to 0, ever other number has one).

Let’s have a look at our numbers again and try to find out what the problem is: We represented a natural number \(n\) by \( \lambda fx.f^{n}x == \lambda fx.f(f(..f(x )..))\) and so to get the predecessor of \(n\) we must “remove” one of the \(f\) if there are any.

Why is this hard?

Have a look at our reduction-rule – it will only replace some variables by something different and there is no way to substitute it with an empty term (as there are no empty terms in lambda calculus).

So you might be tempted to think that this is not possible, It is said that Church himself believed for some time that this is not possible but his student Kleene came to the solution while visiting his dentist – that’s why the trick is called “wisdom tooth trick”.

The Trick

So what is the “trick”?

If you know it it’s indeed rather easy: You cannot remove a \(f\) so you don’t. Instead you start by zero and count up to the number you want the predecessor of BUT by doing this you remember the last number you saw just before. Having reached the desired number you return the memorized last number … doh you might think – that is exactly how I find the predecessor of an character in the alphabet. Well ok – that is my way for most characters and that is because I – like every other person – do remember the ABC…Z series very well but seem not to have the mental capacity to remember the reversed series as well, so to find the predecessor of Q (I remember in triples so T would be to easy) I count up to Q: ABC…MNOPQ and having this still in cache I present you with P”

The More technical points

So first we have to find some way to remember a value and treat a state through our terms. This is where intuition from functional programming comes in handy.

Instead of globally remembering some values we use a tuple as the object we want to manipulate. The first item of this tuple shall be the last number and the second one the current number: $$ (lastNumber, currentNumber) $$ and a step in our algorithm is just $$ (lN, cN) \Rightarrow (cN, Succ cN) $$.

Of course now we have to find a way to create pairs and from a pair get the first and second item.

Making and using Pairs

Just as with the numbers a nice way to do this is using passed functions in a clever way. To create a pair we will use this lambda-calculus term: $$ MkPair := \lambda ab. \lambda s.(s a b)$$. Where \(a\) is the first item in the pair and \(b\) is the second item. Of \(s\) you should think as a “selector” function.

Now defining a selector-function for “first” and “second” is a piece of cake: $$Fst := \lambda ab.a$$ and $$ Snd := \lambda ab.b$$.

To test this let’s say we have a pair \(P := MkPair\ a b == \lambda s.(s a b)\) then using the second-selector we have $$ P\ Snd == \left( \lambda s.(s a b) \right) Snd == Snd\ a b$$ $$ == \left( \lambda xy.y \right) a b == \left( \lambda y.y \right) b == b$$

The transition function

Now we go on and define a term that can transform our \( (lastNumber, currentNumber) \) pairs: given such a pair we have to create a new one, that has the old second item as first item and puts the incremented second item in second place. Using the functions we got so far this is not difficult: $$Trans := \lambda p.MkPair\ (p\ Snd) \ (Succ(p\ Snd))$$

Putting it all together

So now if we only use this function \(n\)-times on \( (Zero, Zero) \) we can use the first item of the result to define the Pred operation. Luckily our number representation is more or less just a for loop so the final operation is $$ Pred := \lambda n.\left( n\ Trans\ (MkPair \ N0\ N0)\right) Fst$$

Testing this with the console interpreter

LAMBDA CALCULUS INTERPRETER
===========================
>>> ?load "c:\temp\mitpred.lcs"
\fx.x
== [N0]

\nfx.(f(nfx))
== [Succ]

\fx.(fx)
== [N1]

\fx.(f^{2} x)
== [N2]

\fx.(f^{3} x)
== [N3]

\fx.(f^{4} x)
== [N4]

\fx.(f^{5} x)
== [N5]

\fx.(f^{6} x)
== [N6]

\fx.(f^{7} x)
== [N7]

\fx.(f^{8} x)
== [N8]

\fx.(f^{9} x)
== [N9]

\fx.(f^{10} x)
== [N10]

\abf.(fab)
== [MkPair]

\ab.a
== [Fst]

\ab.b
== [N0, Snd]

\pf.(f(p\ab.b)\fx.(f(p\ab.bfx)))
== [Trans]

\n.(n\pf.(f(p\ab.b)\fx.(f(p\ab.bfx)))\f.(f\fx.x\fx.x)\ab.a)
== [Pred]

>>> Pred N8
\f_x.(f^{7} _x)
== [N7]

>>> Pred N10
\f_x.(f^{9} _x)
== [N9]


>>> Pred N1
\fx.x
== [N0, Snd]

>>> Pred N0
\fx.x
== [N0, Snd]

And there it is!

Defining the subtraction

This should be trivial by now: subtracting \(m\) from any number \(n\) is the same as finding the \(m\)-th predecessor of this number, and as our numbers are for-loops in disguise this is easy: $$Subt := \lambda nm.m\ Pred\ n$$.

(Do be precise: this is not indeed subtraction because we have no predecessors of zero, but to be even more pedantic: the natural numbers do not really have a meaningful subtraction – those numbers are not even a group under addition)

>>> Subt := \nm.m Pred n
\nm.(m\n.(n\pf.(f(p\ab.b)\fx.(f(p\ab.bfx)))\f.(f\fx.x\fx.x)\ab.a)n)
== [Subt]

>>> Subt N2 N0
\fx.(f^{2} x)
== [N2]

>>> Subt N4 N2
\fx.(f^{2} x)
== [N2]

>>> Subt N2 N4
\fx.x
== [N0, Snd]

Conclusion

So as always this hard problem proved to be quite simple as soon as you know how. Maybe you even tried to find the solution yourself – if you did and did indeed mange to find it: congratulations – you might be a genius (for myself I have to confess: after trying for half an hour or so I went the easy way and asked google/wiki – what a shame, it looks like I might have found it … or not – will never know now)

I hope you enjoyed this one – I surely did – stay tuned for the next part.