Chapter 4: Church Numerals: Decrement

Predecessor

The implementation of the predecessor function is much harder than previous ones. In fact, Church thought for a long time that it might not be possible, until his student Kleene found it. In fact, there is a legend that Kleene conceived the idea while visiting his dentist, which is why the trick is called the wisdom tooth trick.

Wisdom Tooth Trick

Let's define a helper function $\Phi$:

$$\Phi=\lambda p.\pi(S(\pi_1p))(\pi_1p)$$

Initially, we have:

$$\Phi(\pi0\space0)=(\pi1\space0)$$

By means of mathematical induction, we get:

$$\Phi^n(\pi0\space0)=(\pi n\space (n-1))$$

With the help of ordered pair, predecessor function could be defined as:

$$\text{pred}=\lambda n.\pi_2(n\Phi(\pi0\space 0))\\ \text{pred }n=n-1$$

Note that $\text{pred }0=0$. It is a limit of church numerals. Is it possible to define negative numbers or even rational numbers? Of course! Remember what I mentioned in Data Abstraction part? Build one if it doesn't exist yet!

Subtraction

Subtraction compared to predecessor is similar to addition compared to successuor.

$$\text{sub}=\lambda mn.n\text{ pred }m\\ \text{sub }mn=m-n$$

It reads as if "evaluating $n^\text{th}$ predecessor of $m$".

Proof is similar to the addition operation.

Note: if $m<n$, $\text{sub }mn=0$ according to the definition of predecessor function.

Zero Predicate

Let's review the definitions of false and zero:

$$F=\lambda xy.y\\ 0=\lambda s.\lambda z.z$$

With $\alpha$ reduction, it is clear that:

$$F=0=\lambda x.I$$

where $I=\lambda x.x$, called identity function, which returns its parameter unchanged.

Then, $0$ predicate could be defined as:

$$\text{is-zero}=\lambda n.nF\text{ not }F\\$$

Proof:

For $n=0$:

$$\begin{array}{} \text{is-zero }0&=&\text{is-zero }F\\ &=&(\lambda n.nF\text{ not }F)F\\ &=&FF\text{ not }F\\ &=&\text{not }F\\ &=&T \end{array}\\$$

For $n>0$:

$$\begin{array}{} \text{is-zero }n&=&(\lambda n.nF\text{ not }F)n\\ &=&nF\text{ not }F\\ &=&F^n(\text{not})F\\ &=&(\lambda x.I)^n(\text{not})F\\ &=&(\lambda x.I)^{n-1}(I)F\\ &=&\cdots\\ &=&IF\\ &=&F \end{array}$$

Comparison

Subtraction is a fundamental approach to compare two numbers. With the help of the fact that if $m\leq n$, $\text{sub }mn=0$, less-equal function could be defined as:

$$\le:\text{le}=\lambda mn.\text{is-zero}(\text{sub }mn)$$

Since:

$$x\le y\land y \le x \rightarrow x=y$$

Equality function could be defined as:

$$=:\text{eq}=\lambda mn.(\text{and}(\text{le }mn)(\text{le }nm))$$

Rest part of work should be easy now.

$$\begin{array}{} \ge:&\text{ge}&=&\lambda mn.\text{le }nm\\ >:&\text{gt}&=&\lambda mn.\text{not}(\text{le }mn)\\ <:&\text{lt}&=&\lambda mn.\text{gt }nm\\ \ne:&\text{ne}&=&\lambda mn.\text{not}(\text{eq }mn) \end{array}$$