Exercise 2.6
(a) Prove that the following pre-typed λ-term is legal, using the tree format:
$$λx : ((α →β) →α). x(λz : α. y)$$
(b) Transform the derivation into flag format.
For clarity, it is useful to write the lambda term without the types:
$$λx. x(λz. y)$$
(a) To prove the pre-typed λ-term is legal, we need to show there exists a context $Γ$ and type $ρ$ such that $Γ \vdash M : ρ$, where $M$ is the given λ-term.
Let's try the following context
$$Γ := x: (α →β) →α, y: β, z:α$$
We'll now try to apply the 3 Derivation rules of simply typed calculus from Definition 2.4.5, which are (var), (appl) and (abst).
$(i) \quad x: (α →β) →α, \; y: β, z:α \quad \vdash \quad y: β \quad $ (var)
$(ii) \quad x: (α →β) →α, y: β \quad \vdash \quad λz:α.y : α→β \quad $ (abst) on (i)
$(iii) \quad x: (α →β) →α, \; y: β \quad \vdash \quad x: (α →β) →α \quad $ (var)
$(iv) \quad x: (α →β) →α, \; y: β \quad \vdash \quad x(λz:α.y): α \quad $ (appl) on (iii) and (ii)
$(v) \quad y: β \quad \vdash \quad (iv) \quad λx : ((α →β) →α). x(λz:α.y): ((α →β) →α) → α \quad $ (abst) on (iv)
Through an application of the Derivation rules, we've shown there exists a context $Γ$ and type $ρ$ such that $Γ \vdash M : ρ$. The context is $Γ := x: (α →β) →α, y: β, z:α$ and the type is $ρ := α$. This means the λ-term is indeed legal.
The following is a tree diagram summarising the structure of the proof (click to enlarge).
(b) The following is the derivation in flag format (click to enlarge).
