# 22章

## 22.2.3 演習問題

下記の項に対し、空の文脈での解(solution)を3つ見つけよ。

λx:X. λy:Y. λz:Z. (x z) (y z)

### 回答

σΓ $\vdash$ σt : T を満たす (σ, T) を求める。

σ = [X $\mapsto$ Z → A → B, Y $\mapsto$ Z → A]
T = B

σ = [X $\mapsto$ Nat → A → B, Y $\mapsto$ Nat → A, Z $\mapsto$ Nat]
T = B

σ = [X $\mapsto$ Z → (Nat → Nat) → B, Y $\mapsto$ Z → Nat → Nat]
T = B

## 22.5.2 演習問題

次の項に対する principal type を求めよ。

λx:X. λy:Y. λz:Z. (x z) (y z)

### 回答

X → Y → Z → P
(Z → A) → (Z → B) → Z → P
(Z → B → C) → (Z → B) → Z → C

T = (Z → B → C) → (Z → B) → Z → C
σ = (X $\mapsto$ Z　→ B → C, Y $\mapsto$ Z → B)

σt = λx:Z→B→C. λy:Z→B. λz:Z. (x z) (y z)
$\emptyset \vdash$ σt : T なので (σ,T) は solution である.

(σ', T') が別の solution だったとする。すなわち $\emptyset \vdash$ σ't : T'
σ't = λx:σ'(X).λy:σ'(Y).λz:σ'(Z). (x z) (y z)
inversion lemma より T' = $σ'(X) → σ'(Y) → σ'(Z) → T_1$ とおける。
(x:σ'(X), y:σ'(Y), z:σ'(Z)) $\vdash$ (x z) (y z) : $T_1$ なので inversion lemma より
(x:σ'(X), y:σ'(Y), z:σ'(Z)) $\vdash$ (x z) : $T_2 → T_1$ かつ
(x:σ'(X), y:σ'(Y), z:σ'(Z)) $\vdash$ (y z) : $T_2$ とおける.
さらにそれぞれ inversion lemma を使うと
(x:σ'(X), y:σ'(Y), z:σ'(Z)) $\vdash$ x : $T_3 → T_2 → T_1$
(x:σ'(X), y:σ'(Y), z:σ'(Z)) $\vdash$ z : $T_3$
(x:σ'(X), y:σ'(Y), z:σ'(Z)) $\vdash$ y : $T_4 → T_2$
(x:σ'(X), y:σ'(Y), z:σ'(Z)) $\vdash$ y : $T_4$ とおける.
それぞれ inversion lemma を使うと
σ'(X) = $T_3 → T_2 → T_1$
σ'(Y) = $T_4 → T_2$
σ'(Z) = $T_3$ = $T_4$
よって、σ' = γ' $\circ$ (X $\mapsto T_3 → T_2 → T_1$, Y $\mapsto T_3 → T_2$, Z $\mapsto T_3$) とおける。
以上より
σ' = γ' $\circ$ (Z$\mapsto T_3$, B $\mapsto T_2$, C $\mapsto T_1$) $\circ$ σ となるので $σ \sqsubseteq σ'$.