Exercise 2.13
Find a term of type $τ$ in context $Γ$, with:
(a) $τ ≡(α →β) →α →γ, \quad Γ ≡x : α →β →γ$
(b) $τ ≡α →(α →β) →γ, \quad Γ ≡x : α →β →α →γ$
(c) $τ ≡(α →γ) →(β →α) →γ, \quad Γ ≡x : (β →γ) →γ$
Give appropriate derivations.
(a) The derivation below shows the term is
$$\lambda y:\alpha \to \beta.\lambda z:\alpha.xy$$
such that
$$ x: \alpha \to \beta \to \gamma \quad \vdash \quad \lambda y:\alpha \to \beta.\lambda z:\alpha.xy: (\alpha \to \beta) \to \alpha \to \gamma$$
(b) The derivation below shows the term is
$$ \lambda y:\alpha.\lambda z:\alpha \to \beta.(xz)y $$
such that
$$ x : α →β →α →γ \quad \vdash \quad \lambda y:\alpha.\lambda z:\alpha \to \beta.(xz)y : : \alpha \to (\alpha \to \beta) \to \gamma $$
(c) The derivation below shows the term is
$$ \lambda y: \alpha \to \gamma.\lambda z:\beta \to \alpha.(xz)y $$
such that
$$ x: (\beta \to \gamma) \to \beta \quad \vdash \quad \lambda y: \alpha \to \gamma.\lambda z:\beta \to \alpha.(xz)y: ( \alpha \to \gamma) \to (\beta \to \alpha) \to \gamma $$
