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))) THREE = ADD1(ADD1(ADD1(ZERO))) FIVE = ADD1(ADD1(ADD1(ADD1(ADD1(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)) `

**Question:**

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.