Exercise 3.16
See the previous exercises. Find λ2-terms that represent the logical operators ‘inclusive or’, ‘exclusive or’ and ‘implication’.
The Wikipedia page helps think about what logical operators must do (link). This page is also helpful (link). This thinking tells us a logical conjunction operating on two Booleans $p,q$ must return $q$ if $p$ is true, else return $p$, which would be false in this case. That is, $pqp$,
Using this we can look afresh at the λ2 generalisation to see how it does this.
$$M ≡λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβyy)$$
If $u$ is true, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false).
If $u$ is false, then we select $(vβyy)$ and regardless of $v$ we pick $y$ (false).
Inclusive Or
Using the linked pages, we can see a logical disjunction operating on two Booleans $p, q$ must return $p$ if $p$ is true, else return $q$, where the value of $q$ becomes the final result. That is, $ppq$.
We generalise this to λ2 as follows.
$$M ≡λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxx)(vβxy)$$
If $u$ is true, then we select $(vβxx)$ and regardless of $v$ is true we pick $x$ (true).
If $u$ is false, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false).
Exclusive Or
A logical exclusive or operating on two Booleans $p, q$ must return $\neg q$ if $p$ is true, else return $q$, where the value of $q$ becomes the final result. That is, $p(\neg q)q$.
We generalise this to λ2 as follows.
$$M ≡λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβyx)(vβxy)$$
If $u$ is true, then we select $(vβyx)$ and if $v$ is true we pick $y$ (false), else $x$ (true).
If $u$ is false, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false).
Implication
A logical implication operating (link) on two Booleans $p, q$ always returns true, except if $p$ is true and $q$ is false. That is, $pqq$.
We generalise this to λ2 as follows.
$$M ≡λu,v : Bool . λβ : ∗. λx,y : β. uβ(vβxy)(vβxx)$$
If $u$ is true, then we select $(vβxy)$ and if $v$ is true we pick $x$ (true), else $y$ (false).
If $u$ is false, then we select $(vβxx)$ and regardless of $v$ we pick $x$ (true).
