Exercise 2.8
(a) Add types to the bound variables in the λ-term $λxy. y(λz. yx)$ such that the type of this term becomes
$$(γ →β) →((γ →β) →β) →β$$
(b) Give a derivation in tree format, proving this.
(c) Sketch a diagram of the tree structure, as in Section 2.5.
(d) Transform the derivation into flag format.
(a) Let's first establish the types variables, all of which happen to be bound. The desired term tells us the type of $x$ and $y$. These are $x:γ → β$ and $y:((γ→β)→β)$. We can use these to narrow down the type of $z$. Lets label the type of $z$ as $α$.
Given these known types, the type of $yx$ must be $β$. The type of $(λz.yx)$ must therefor be $α→β$. Since $y:((γ→β)→β)$ is applied to $(λz.yx):α→β$, this tells us $γ=α$.
To summarise, pre-typed λ-term is.
$$λx:γ→β.y:(γ→β)→β. y(λz:γ. yx)$$
(b) The following is derivation to confirm the type of the above γ-term.
(i) (var) gives us x:γ→β
(ii) (var) gives us y:(γ→β)→β
(iii) (appl) on (i) and (ii) gives us yx:β
(iv) (abst) gives us λz.yx:γ→β
(v) (appl) on (iv) and (ii) gives us $y(λz. yx):β$
(vi) (abst) gives us $λy.y(λz. yx):((γ→β)→β)→β$
(vii) (abst) gives us $λxy.y(λz. yx):(γ→β)→((γ→β)→β)→β$ as required.
(c) The following is a tree diagram showing the structure of the proof (click to enlarge).
(d) The following is the derivation in flag-format (click to enlarge).
