Exercise 1.9
Consider the following λ-terms (cf. Section 1.12):
$K := λxy. x$
$S := λxyz. xz(yz)$
(a) Check that $K P Q \to _β P$ and $S P QR \to _ β P R(QR)$, for arbitrary λ-terms $P$, $Q$ and $R$.
(b) Let $I := λx. x$. Prove that $S K K \to _β I$.
(c) Let $B := S(K S)K$. Prove that $B U V W \to _β U(V W)$.
(d) Prove that $S S S K K=_β S K K K$.
(a) Let's start with $K P Q$,
$$\begin{align} K P Q & = (\lambda xy . x) P \; Q\\ \\ & = (\lambda x . (\lambda y . x)) P \; Q \\ \\ & \to (\lambda y . P) Q \\ \\ & \to P \end{align}$$
Now let's consider $S P Q R$
$$\begin{align} S P Q R & = (\lambda x y z . xz(yz)) P \; Q \; R \\ \\ & = (\lambda x . (\lambda y . (\lambda z . (xz (yz) )))) P \; Q \; R \\ \\ & \to (\lambda y . (\lambda z . (P z (y z) ))) Q \; R \\ \\ & \to (\lambda z . (P z (Qz) )) R \\ \\ & \to P R (Q R) \end{align} $$
(b) We note that $I:= \lambda x.x$ is the identity function.
$$\begin{align} S K K & = (λx y z. x z (y z)) (λab. a) (λcd. c) \\ \\ & \to ( λy z. (λab. a) z(y z) ) (λcd. c) \\ \\ & \to ( λz. (λab. a) z( (λcd. c) z) ) \\ \\ & \to ( λz.z) \end{align}$$
(c) This is algebra torture, but we'll proceed carefully.
$$\begin{align} S (K S) K & = (\lambda x y z . x z (y z) ) (K S) K \\ \\ &\to (\lambda y z . (K S) z (y z) ) K \\ \\ & \to (\lambda z . (K S) z (K z) ) \\ \\ & \to (\lambda z . ((\lambda a b . a) (\lambda u v w . u w (v w))) z ( (\lambda a b . a) z) ) \\ \\ & \to (\lambda z . (\lambda u v w . u w (v w)) ( (\lambda a b . a) z) ) \\ \\ & \to (\lambda z . (\lambda v w . ( (\lambda a b . a) z) w (v w) ) ) \\ \\ & \to (\lambda z . (\lambda v w . z (vw) ) ) \\ \\ & = (\lambda z v w . z (v w)) \end{align}$$
So
$$(\lambda z v w . z (v w)) \; U V W \to U (V W)$$
(d) Again, algebra torture. Here we need to show the two expressions reduce to the same β-normal-form.
First we consider $S S S K K$.
$$\begin{align} S S S K K & = ( ( (S S) S) K ) K \\ \\ & = ( ( ( (λxyz. xz(yz)) (λabc. ac(bc))) (λuvw. uw(vw))) (λjk. j) ) (λmn. m) \\ \\ & \to ( ( (λyz. (λabc. ac(bc))z(yz) ) (λuvw. uw(vw))) (λjk. j) ) (λmn. m) \\ \\ & \to ( λz. (λabc. ac(bc))z( (λuvw. uw(vw)) z) ) (λjk. j) (λmn. m) \\ \\ & \to (λabc. ac(bc)) (λjk. j) ( (λuvw. uw(vw)) (λjk. j)) (λmn. m) \\ \\ & \to (λjk. j) (λmn. m) ( ( (λuvw. uw(vw)) (λjk. j)) (λmn. m) ) \\ \\ & \to (λmn. m) \end{align}$$
Next we consider $S K K K$. Note that $S K K K = I$, so the expression reduces to just $K$ which is $λxy. x$, the same as what the first expression reduces to.
Since the two expressions reduce to the same normal form, they are β-equivalent.
