Exercise 1.10
We define the λ-terms zero, one, two (the first three so-called Church numerals), and the λ-terms add and mult (which mimic addition and multiplication of Church numerals) by:
zero := $λfx. x$
one := $λfx. f x$
two := $λfx. f(f x)$
add := $λmnfx. mf(nf x)$
mult := $λmnfx. m(nf)x$
(a) Show that add one one $\to _β$ two.
(b) Prove that add one one $\neq_β$ mult one zero.
(a) We do this by β-reduction.
$$\begin{align} add\;one\;one&= (λmnfx. mf(nf x)) \; (λgy. g y) \; (λhz. h z) \\ \\ & \to λfx. (λgy. g y)f( (λhz. h z)f x) \\ \\ & \to λfx. (λgy. g y)f( (λhz. h z)f x) \\ \\ & \to λfx. (λgy. g y)f(f x) \\ \\ & \to λfx.f(f x) \\ \\ & = two \end{align}$$
(b) Again we do this by β-reduction, and show the result is not two.
$$\begin{align} mult \; one \; zero &= (λmnfx. m(nf)x) (λgy. g y) (λhz. z) \\ \\ & \to (λfx. (λgy. g y)((λhz. z)f)x) \\ \\ & \to (λfx.((λhz. z)f)x) \\ \\ & \to (λfx.x) \\ \\ & = zero \end{align}$$
The expression reduces to zero, which is correct, and not two.
Exercise 1.11
The successor is the function mapping natural number $n$ to $n+1$. It is represented in λ-calculus by $suc := λmf x. f(mf x)$. Check the following for the Church numerals defined in the previous exercise:
(a) $suc \; zero =_β one$
(b) $suc \; one =_β two$
(a)
$$\begin{align} suc \; zero & = (λmf x. f(mf x)) (λgy. y) \\ \\ & \to (λf x. f( (λgy. y)f x)) \\ \\ & \to (λf x. f x) \\ \\ & = one \end{align}$$
(b)
$$\begin{align} suc \; one & = (λmf x. f(mf x)) (λgy. fy) \\ \\ & \to (λf x. f((λgy. fy)f x)) \\ \\ & \to (λf x. f(f x)) \\ \\ & = two \end{align}$$
