I am trying to "reinvent" Kleene's predecessor myself. The following code snippet should be self-explanatory. The idea is to make a 2-tuple and count up from zero, i.e. lambda f: lambda x: x, as described in this article:

#!/usr/bin/env python3

NULL = lambda x: x
ZERO = lambda f: lambda x: x

TRUE = lambda T: lambda F: T(NULL)
FALSE = lambda T: lambda F: F(NULL)
IF_ELSE = lambda cond: lambda T: lambda F: cond(T)(F)
IS_ZERO = lambda n: n(lambda _: FALSE)(TRUE)

ADD1 = lambda n: lambda f: lambda x: f(n(f)(x))

MakePair = lambda first: lambda second: lambda cond: IF_ELSE(cond)(lambda x: first)(lambda x: second)
First = lambda pair: pair(TRUE)
Second = lambda pair: pair(FALSE)
Trans = lambda pair: lambda cond: IF_ELSE(cond)(lambda x: Second(pair))(lambda x: ADD1(Second(pair)))
SUB1 = lambda n: First(n(Trans)(MakePair(ZERO)(ZERO)))


if __name__ == '__main__':
    print(SUB1(THREE)(lambda x: x + 1)(0))
    print(SUB1(FIVE)(lambda x: x + 1)(0))

In the end, the linked article notes that

It is then straightforward but tedious to expand all of the short-hand expressions above, and reduce the resulting expression to normal form. This results in the standard magical encoding of predecessor.

I assume the normal form of Kleene's predecessor looks like this:

pred = lambda n: lambda f: lambda x: n (lambda g: lambda h: h (g (f))) (lambda y: x) (lambda x: x)

However, after applying a series of expansion and $\beta$-reduction, I ended up with this:

SUB1 = lambda n: n(lambda pair: lambda cond: cond(lambda x: pair(lambda T: lambda F: F(NULL)))(lambda x: lambda f: lambda x: f((pair(lambda T: lambda F: F(NULL)))(f)(x))))(lambda _: lambda f: lambda x: x)(lambda T: lambda F: T(lambda x: x))


How do I reduce my SUB1 function to pred? I don't think we can go further with only $\beta$-reduction, and there must be some advanced reduction techniques unknown to me.

A step-by-step solution would be greatly appreciated. Note that this is not a homework problem though; I am doing the exercise just for fun.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.