Exercise 3.15
See Exercise 3.14. Define $M$ by
$$M ≡λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy)$$
(a) Reduce the following terms to β-normal form:
$M \; True \; True$
$M \; True \; False$
$M \; False \; True$
$M \; False \; False$
(b) Which logical operator is represented by $M$?
(a) Let's do each in turn.
First $M \; True \; True$.
$$\begin{align} M \; True \; True & \equiv λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (True) \; (True) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (True)β \; ((True)βxy) \; ((True)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. x)β \; ((λα : ∗. λx,y : α. x)βxy) \; ((λα : ∗. λx,y : α. x)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. x) \; ((λx,y : β. x)xy) \; ((λx,y : β. x)yy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. x)xy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. x \\ \\ &=_\beta True \end{align}$$
Next $M \; True \; False$.
$$\begin{align} M \; True \; True & \equiv λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (True) \; (False) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (True)β \; ((False)βxy) \; ((False)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. x)β \; ((λα : ∗. λx,y : α. y)βxy) \; ((λα : ∗. λx,y : α. y)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. x) \; ((λx,y : β. y)xy) \; ((λx,y : β. y)yy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. y)xy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. y \\ \\ &=_\beta False \end{align}$$
Now $M \; False \; True$.
$$\begin{align} M \; True \; True & \equiv λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (False) \; (True) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (False)β \; ((True)βxy) \; ((True)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. y)β \; ((λα : ∗. λx,y : α. x)βxy) \; ((λα : ∗. λx,y : α. x)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. y) \; ((λx,y : β. x)xy) \; ((λx,y : β. x)yy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. x)yy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. x \\ \\ &=_\beta False \end{align}$$
Finally, $M \; False \; False$
$$\begin{align} M \; True \; True & \equiv λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy) \; (False) \; (False) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (False)β \; ((False)βxy) \; ((False)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λα : ∗. λx,y : α. y)β \; ((λα : ∗. λx,y : α. y)βxy) \; ((λα : ∗. λx,y : α. y)βyy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. (λx,y : β. y) \; ((λx,y : β. y)xy) \; ((λx,y : β. y)yy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. ((λx,y : β. y)xy) \\ \\ &\to_\beta λβ : ∗. λx,y : β. y \\ \\ &=_\beta False \end{align}$$
(b) $M$ behaves as the logical conjunction $\land$, also written as "AND".
