Exercise 3.17
See the previous exercises. Find a λ2-term $Iszero$ that represents the test-for-zero. That is, define a λ2-term such that $Iszero \; Zero =_β True$ and $Iszero \; n =_β False$ for all polymorphic Church numerals $n$ except $Zero$. (Hint: see Exercise 1.14)
Let's remind ourselves of some definitions.
The Church booleans.
$Bool ≡Πα : ∗. α →α →α$
$True ≡λα : ∗. λx,y : α. x$
$False ≡λα : ∗. λx,y : α. y$
The Church numerals.
$Nat ≡ Πα : ∗. (α →α) →α →α$
$Zero ≡ λα : ∗. λf : α →α. λx : α. x$
$One ≡ λα : ∗. λf : α →α. λx : α. f x$
$Two ≡ λα : ∗. λf : α →α. λx : α. f(f x)$
From Exercise 1.13, we have the untyped $iszero := λz. z(λx. \; false) \; true$.
The key to how it works is that zero $λfx.x$ applied to $(λx. \; false) (true)$ picks $true$, and any non-zero Church numeral $λfx.f^{n}x$ picks $false$. This is the mechanism we need to re-use in our generalisation to λ2.
Comparing the λ2 Church numerals with the selection mechanism above, we see we need to resolve the type variable $λα : ∗$ leaving a term that takes two parameters $ λf : α →α. λx : α$.
$$Iszero \equiv λz:Nat.z(Bool)(λx:Bool. \; False) \; True $$
The type of $x$ as $Bool$ is required because $(λx. \; False)$ needs to be $Bool \to Bool$, and that requires the type argument to $z$ also needs to be $Bool$ such that the $f$ in the Church numerals is $Bool \to Bool$.
Let's check $Iszero \; Zero =_β True$.
$$\begin{align} Iszero \; Zero &\equiv (λz:Nat.z(Bool)(λx: Bool. \; False) \; True ) \; Zero \\ \\ & =_β (Zero)(Bool)(λx:Bool. \; False) \; True \\ \\ & =_β (λf : Bool →Bool. λx : Bool. x)(λx: Bool. \; False) \; True \\ \\ & =_β True \end{align}$$
Let's also check $Iszero \; One =_β False$.
$$\begin{align} Iszero \; One &\equiv (λz:Nat.z(Bool)(λx: Bool. \; False) \; True ) \; One \\ \\ & =_β (One)(Bool)(λx:Bool. \; False) \; True \\ \\ & =_β (λf : Bool →Bool. λx : Bool. fx)(λx: Bool. \; False) \; True \\ \\ & =_β False \end{align}$$
