predecessor and multiplication prove

Question

I have trouble, when attempting to :

1- prove mult defines the multiplication function.

2- Prove pred defines the predecessor function.

1- for mult:

Base Case:

mult 0x= 0

Inductive case:

:= $(\lambda m. \lambda n. \lambda f . \lambda x.m (nf)x) (\lambda f. \lambda x.x)(\lambda fx. \lambda x.(f^{(n)} x))$

the result is $(\lambda f. \lambda x.x)$.

2- for pred:

Base Case:

f(0,..)= 0

Inductive case:

$\lambda n.\lambda f. \lambda x.n (\lambda g. \lambda h.h (gf)) (\lambda u.x)( \lambda u.u)$.

(f(s(x),..) = n-1

And I am unsure of where to go from there, because I have no parameters for the n to be n-1.

Answer 1

The proof that the term $\text{pred}$ encodes the predecessor function over natural numbers is quite technical and requires a lemma.

For any $n \in \mathbb{N}$, let $\underline{n} = \lambda f \lambda x. f^{n} x = \lambda f \lambda x. \overbrace{f (\cdots (f}^{n \text{ times}} x) \cdots)$ (in particular, $\underline{0} = \lambda f \lambda x.x$).

Lemma. Given $n \in \mathbb{N}$, $(\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x)$ reduces to $\lambda h.h (f^n x)$

Proof. By induction on $n \in \mathbb{N}$.

• Base case ($n = 0$):

\begin{align} (\lambda g \lambda h.h (g f)) (\lambda u.x) \to \lambda h.h ((\lambda u.x) f) \to \lambda h.h x \,. \end{align}

• Inductive step: we suppose that $(\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x)$ reduces to $\lambda h.h (f^n x) \, $ (induction hypothesis) and we show that $(\lambda g \lambda h.h (g f))^{n+2} (\lambda u.x)$ reduces to $\lambda h.h (f^{n+1} x)$.

\begin{align} (\lambda g \lambda h.h (g f))^{n+2} (\lambda u.x) &= (\lambda g \lambda h.h (g f)) \big((\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x) \big) \\ &\to^* (\lambda g \lambda h.h (g f)) (\lambda h.h (f^n x)) \quad \text{(by induction hypothesis)} \\ & \to \lambda h.h ((\lambda h.h (f^nx)) f) \to \lambda h.h (f (f^n x)) = \lambda h.h (f^{n+1} x) \, .\\ &\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \square \end{align}

Let $\text{pred} = \lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u)$. Thanks to the lemma above, let us show that the term $\text{pred}$ encodes the predecessor function over natural numbers, i.e. that $\text{pred} \, \underline{0}$ reduces to $\underline{0}$, and $\text{pred} \, \underline{n+1}$ reduces to $\underline{n}$ for any $n \in \mathbb{N}$.

• Case $n = 0$: \begin{align} \text{pred} \, \underline{0} =& \ \big(\lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \big) \lambda f \lambda x.x \\ \to& \ \lambda f \lambda x. (\lambda f' \lambda x'.x') (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda x'.x') (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. x = \underline{0} \end{align}

• Case $n + 1$: \begin{align} \text{pred} \, \underline{n+1} =& \ \big(\lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \big) \lambda f \lambda x. f^{n+1}x \\ \to& \ \lambda f \lambda x. (\lambda f' \lambda x'. (f')^{n+1}x') (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda x'. (\lambda g \lambda h.h (g f))^{n+1} x') (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda h. h (f^n x)) (\lambda u.u) \quad \text{(by the lemma)}\\ \to& \ \lambda f \lambda x. (\lambda u.u) (f^n x) \\ \to& \ \lambda f \lambda x. f^n x = \underline{n} \, . \end{align}

---

The proof that the term $\text{mult}$ encodes the multiplication function over natural numbers is similar to (and slightly simpler than) the proof above.