Chapter 3: Church Numerals: Increment

Church Numerals

The most important data in computer programs are integers.

Let's define natural integers.

$$0=\lambda s.\lambda z.z\\ 1=\lambda s.\lambda z.s(z)\\ 2=\lambda s.\lambda z.s(s(z))\\ 3=\lambda s.\lambda z.s(s(s(z)))\\ \vdots\\ n=\lambda s.\lambda z.s^n(z)$$

Why should we define integers like this? What does $s$ and $z$ mean here?

Let's take $2$ for example to watch how church numerals could be converted back to normal ones. let $s=\lambda x.(x+1), z=0$, then:

$$\begin{array}{} 2sz&=&(\lambda s.\lambda z.s(s(z)))sz\\ &=&s(s(z))\\ &=&s(s(0))\\ &=&s(0+1)\\ &=&1+1\\ &=&2\\ \end{array}$$

It is clear now: $s$ stands for succussor and $z$ stands for zero. It is built base on recursion. And yes, it is exactly how natural numbers are defined mathematically.

Successor

To get the successor of a church numeral, just simply wrap an $s$ around it.

$$S=\lambda n.\lambda s.\lambda z.(s(nsz))\\ Sn=n+1$$

Proof:

$$\begin{array}{} Sn&=&(\lambda n.\lambda s.\lambda z.(s(nsz)))(\lambda s.\lambda z.s^n(z))\\ &=&(\lambda s'.\lambda z'.(s'((\lambda s.\lambda z.s^n(z))s'z')))\\ &=&(\lambda s'.\lambda z'.(s'(s'^n(z'))))\\ &=&(\lambda s'.\lambda z'.(s'^{n+1}(z')))\\ &=&(\lambda s.\lambda z.(s^{n+1}(z)))\\ &=&n+1\\ \end{array}$$

Addition

A Church numeral $n$ is actually a recursion builder repeating a function for $n$ times. Making use of this the addition operation of church numerals could be deduced.

$$\text{add}=\lambda mn.(mSn)\\ \text{add }mn=m+n$$

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

Proof:

$$\begin{array}{} \text{add }mn&=&(\lambda mn.(mSn))mn\\ &=&(\lambda s.\lambda z.s^m(z))S(\lambda s.\lambda z.s^n(z))\\ &=&\lambda z.S^m(z)(\lambda s.\lambda z.s^n(z))\\ &=&S^m(\lambda s.\lambda z.s^n(z))\\ &=&\lambda s.\lambda z.s^{m+n}(z)\\ &=&m+n\\ \end{array}$$

Actually, there is a direct definition of addition.

$$\text{add}=\lambda m.\lambda n.\lambda s.\lambda z.ms(nsz)\\$$

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

Proof is similar to indirect one.

Multiplication

Indirect definition:

$$\text{mul}=\lambda mn.m(\text{add }n)0\\ \text{mul }mn=m\times n$$

It reads as if "add $n$ for $m$ times to $0$".

Direct definition:

$$\text{mul}=\lambda m.\lambda n.\lambda s.\lambda z.m(ns)z$$

It reads as if "'evaluating $n^\text{th}$ successor' for $m$ times of $0$".

Proofs are similar to the addition operation.

Exponentiation

Indirect definition:

$$\text{exp}=\lambda mn.n(\text{mul }m)1\\ \text{exp }mn=m^n$$

It reads as if "multiplies $m$ for $n$ times to $1$".

Proof is similar to the multiplication operation.

Direct definition:

$$\text{exp}=\lambda m.\lambda n.\lambda s.\lambda z.nmsz$$

Or just

$$\text{exp}=\lambda m.\lambda n.nm$$

for short.

Proof:

$$\begin{array}{} \text{exp }mn&=&nm\\ &=&(\lambda s.\lambda z.s^n(z))m\\ &=&\lambda z.m^n(z)\\ &=&\lambda s.m^n(s)\\ &=&\lambda s.\lambda z.m^n(s)z\\ &=&\lambda s.\lambda z.\underbrace{m(\cdots m(m}_{n \text{ times}}s))z\\ &=&\lambda s.\lambda z.\underbrace{m(\cdots m(m}_{n-1 \text{ times}}\underbrace{(\lambda z_1.s^m(z_1))}_{\text{apply } s \text{ for } m \text{ times}}))z\\ &=&\lambda s.\lambda z.\underbrace{m(\cdots m(m}_{n-2 \text{ times}}\underbrace{(\lambda z_2.(\lambda z_1.s^m(z_1))^m(z_2)))}_{\text{apply `apply } s \text{ for } m \text{ times' for } m \text{ times}}))z\\ &=&\lambda s.\lambda z.\underbrace{m(\cdots m(m}_{n-2 \text{ times}}\underbrace{(\lambda z_2.(\lambda z_1.s^m(z_1))^m(z_2)))}_{\text{apply } s \text{ for } m\times m=m^2 \text{ times}}))z\\ &=&\cdots\\ &=&\lambda s.\lambda z.\underbrace{\lambda z_n.(\cdots(\lambda z_2.(\lambda z_1.s^m(z_1))^m(z_2))\cdots)^m(z_n)}_{\text{apply } s \text{ for } \underbrace{m\times m \times\cdots \times m}_{n \text{ times}}=m^n \text{ times}}z\\ &=&\lambda s.\lambda z.s^{m^n}(z)\\ &=&m^n \end{array}$$

Sequences

Observe the architecture of sequences and church numerals:

$$\begin{array}{l} &\text{Sequences}&\text{Church Numerals}\\ \text{Initial term}&a_0 & z\\ \text{Recurrence function}&f_{a_{n-1}\rightarrow a_n} & s \end{array}$$

And yes, natural numbers, are no more than a special arithmetic sequence with initial $0$ and successor fucntion $\lambda x.(x+1)$.

Church numerals, however, are unnecessary to be mere natural numbers, not even mere arithmetic sequence, but whatever sequence you want! e. g.

• $s=\lambda x.(x+d), z=a_0$ makes a arithmetic sequence.
• $s=\lambda x.(x\times q), z=a_0 (q\ne0)$ makes a geometric sequence.

Let's prove obscure direct definition of exponentiation via geometric sequence:

$$\text{exp }mn=\lambda s.\lambda z.ns'z'=m^n$$

$s'$ should be a multiplier of $m$, so it should evaluate $m^{\text{th}}$ succussor to $0$, regardless of succussor function, which represents previous result of evaluation.

$$\begin{array}{} s'&=&\lambda x.\lambda z.(m\times x+z)\\ &=&\lambda x.\lambda z.(\underbrace{x+x+\cdots+x}_{m \text{ times}}+z)\\ &=&\lambda s.\lambda z.s^m(z)\\ &=&m \end{array}$$

$z'$ should be one.

$$z'=sz$$

Neat.