Exercise 3.3
Take $M$ as in Exercise 3.2. Assume $nat : ∗$, $bool : ∗$, $suc : nat → nat$ and $even : nat →bool$.
(a) Prove that $M \; nat \; nat \; bool \; suc \; even$ is legal.
(b) Prove that $λx : nat. even (suc \; x)$ is legal, in two ways:
(1) using Exercise 3.3(a) and Subject Reduction; (2) directly.
Let's remind ourselves of $M$,
$$M ≡λα,β,γ : ∗. λf : α →β. λg : β →γ. λx : α. g(f \; x)$$
We have already shown in Exercise 3.2 that $M$ is legal,
$$\emptyset \vdash \alpha, \beta, \gamma : *. \lambda g : \beta \to \gamma . \lambda f : \alpha \to \beta. \lambda x: \alpha . g (fx) : \Pi \alpha, \beta, \gamma : * . (\beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma$$
By the Thinning Lemma, every context $Γ$ entails the same term and type.
(a) We're given $Γ⊢nat:*$ and $Γ⊢bool:*$. Using (appl2) three times gives us
$$Γ⊢ ( α,β,γ:*. λ g : nat \to bool . λ f : nat \to nat. λ x: nat. g (f \; x) ) \; nat \; nat \; bool$$
$$: (nat \to bool) \to (nat \to nat) \to nat\to bool$$
Since $suc : nat → nat$ and $even : nat →bool$ are compatible types, we can use (appl) twice to get
$$Γ⊢ ( α,β,γ:*. λ g : nat \to bool . λ f : nat \to nat. λ x: nat. g (f \; x) ) \; nat \; nat \; bool \; suc \; even \; : nat\to bool$$
We have shown that for any context $Γ$, the term $M \; nat \; nat \; bool \; suc \; even$ has a type $nat \to bool$, and so is legal.
(b) (1) The term $λx : nat. even (suc \; x)$ is β-equivalent to $M \; nat \; nat \; bool \; suc \; even$ which we have shown has type $nat \to bool$, under any context.
So by Subject Reduction, $λx : nat. even (suc \; x)$ also has type $nat \to bool$, under any context, and so is legal.
(b) (2) Direct proof uses the following flag notation.
We have shown that for a context $Γ= nat:*, \; bool:*, \; suc: nat \to nat, \; even : nat \to bool$ the term $λx : nat. even (suc \; x)$ has type $nat \to book$, and so is legal.
