Exercise 3.13
See the previous exercise.
(a) We define $Add$ in λ2 as follows:
$Add ≡λm,n : Nat . λα : ∗. λf : α →α. λx : Nat . mαf(nαf x)$
Show that $Add$ simulates addition, by evaluating $Add \; One \; One$.
(b) Find a λ2-term $Mult$ that simulates multiplication on $Nat$. (Hint: see Exercise 1.10.)
(a) Let's evaluate $Add \; One \; One$.
$$\begin{align} Add \; One \; One & \equiv (λm,n : Nat . λα : ∗. λf : α →α. λx : Nat . mαf(nαf x)) \; (λα : ∗. λf : α →α. λx : α. f x) \; (λα : ∗. λf : α →α. λx : α. f x) \\ \\ & \to_\beta λα : ∗. λf : α →α. λx : Nat . [λα : ∗. λf : α →α. λx : α. f x] αf([λα : ∗. λf : α →α. λx : α. f x] αf x) \\ \\ & \to_\beta λα : ∗. λf : α →α. λx : Nat . [λx : α. f x] ([λx : α. f x]x) \\ \\ & \to_\beta λα : ∗. λf : α →α. λx : Nat . [λx : α. f x] (f x) \\ \\ & \to_\beta λα : ∗. λf : α →α. λx : Nat . [f (fx)] \\ \\ &\to_\beta Two \tag*{$\Box$}\end{align}$$
So $Add \; One \; One$ is indeed $Two$.
Note that I think there is a typo in the textbook, where $λx : Nat$ should be $λx : α$. Further discussion here (link).
(b) From exercise 1.10 we're given $mult := λmnfx. m(nf)x$. From this we can generalise a λ2 $Mult$ as follows.
$$Mult := λm,n:Nat . λα:*. λf:α→α.λx:α. mα(nαf)x$$
Let's test it with $Mult \; One \; Two$.
$$\begin{align} Mult \; One \; Two & \equiv λm,n:Nat . λα:*. λf:α→α.λx:α. mα(nαf)x \; (λα : ∗. λf : α →α. λx : α. f x) \; (λα : ∗. λf : α →α. λx : α. f (fx)) \\ \\ &\to_\beta λα:*. λf:α→α.λx:α. [λα : ∗. λf : α →α. λx : α. f x] α([λα : ∗. λf : α →α. λx : α. f (fx)] αf)x \\ \\ &\to_\beta λα:*. λf:α→α.λx:α. [λf : α →α. λx : α. f x](λx : α. f (fx))x \\ \\ &\to_\beta λα:*. λf:α→α.λx:α. (f (fx)) \\ \\ &\to_\beta Two \tag*{$\Box$} \end{align}$$
So $Mult \; One \; Two$ is indeed $Two$.
