ラムダ計算で型のリハビリ

1. 文脈に束縛を追加するとき、すでに束縛している名前とは別のものを追加する。
2. 文脈のすべての束縛は別々の変数名を持つ。

• 1について、文脈に束縛を追加するのはT-Absだけである。ラムダ抽象の変数を束縛するときに、必要に応じてフレッシュな変数を用いてα-変換することで、名前の衝突を避けられる。
• 2について、1の性質より成り立つ

1. $\Gamma \vdash x : R$ ならば、 $x : R \in \Gamma$ である。
2. $\Gamma \vdash \lambda x : T_1 . ~ t_2 : R$ ならば、$\Gamma , x : T_1 \vdash t_2 : R_2$ を満たす $R_2$ が存在し、 $R = T_1 \rightarrow R_2$ である。
3. $\Gamma \vdash t_1 ~ t_2 : R$ ならば、 $\Gamma \vdash t_1 : T_{11} \rightarrow R$ と $\Gamma \vdash t_2 : T_{11}$ を満たす $T_{11}$ が存在する。
4. $\Gamma \vdash 0 : R$ ならば、 $R = \text{Nat}$ である。
5. $\Gamma \vdash \text{succ} ~ t_1 : R$ ならば、 $R = \text{Nat}$ かつ $\Gamma \vdash t_1 : \text{Nat}$ である。
6. $\Gamma \vdash \text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2 : R$ ならば、 $\Gamma \vdash t_1 : T_1$ と $\Gamma , x : T_1 \vdash t_2 : R$ を満たす $T_1$ が存在する。

概要：ある項にある型が付いているとき、項の形から型の形をいえる補題。

証明：

型付け規則の定義より自明。

1. $v$ が $T_1 \rightarrow T_2$ 型の値ならば、 $v = \lambda x : T_1 . ~ t_2$ である。
2. $v$ が $\text{Nat}$ 型の値ならば、 $v$ は抽象構文にしたがった数値である。

概要：ある値にある型が付いているとき、型の形から値の形をいえる補題。

証明：

抽象構文の定義によれば、値である $v$ は

• $λx:T_1. t$
• $0$
• $\text{succ} ~ \text{nv}$

のいずれかの形。

補題のそれぞれの節について、 $v$ をこれら3つのパターンに分けて検証すれば十分である。

• 1について、
  • $v$ が $λx:T_1. t$ 型の場合、逆転補題2より $T_1 \rightarrow R_2$ 型が付く。そのため前提を満たし、結論も満たす。
  • $v$ が $0$ の場合、逆転補題4より関数型が付かないため前提を満たさない。
  • $v$ が $\text{succ} ~ \text{nv}$ の場合、逆転補題5より関数型が付かないため前提を満たさない。
• 2について、
  • $v$ が $λx:T_1. t$ 型の場合、逆転補題2より $\text{Nat}$ 型が付かないため前提を満たさない。
  • $v$ が $0$ の場合、逆転補題4より $\text{Nat}$ 型が付くため前提を満たす。抽象構文の定義によれば0は数値であるため、結論も満たす。
  • $v$ が $\text{succ} ~ \text{nv}$ の場合、逆転補題5より $\text{Nat}$ 型が付くため前提を満たす。抽象構文の定義によれば $\text{succ} ~ \text{nv}$ は数値であるため、結論も満たす。

$\vdash t : T$ ならば $t$ は値であるか、ある $t'$ が存在して $t \longrightarrow t'$ である。

概要：空の文脈で型が付いた項は値であるか、別の形に評価できる。

証明：

$\vdash t : T$ の導出に関する構造的帰納法によって示す。

• T-Varの場合、
  • 定理とT-Varの結論を以下のように対応付ける（左辺が定理、右辺がT-Varの結論。名前が違う意味で衝突するときは、右辺の名前を優先して変える）
    • $\varnothing = \Gamma$
  • 空の文脈でT-Verに型は付けられないため、定理の前提は成立せず、所望の結論は自明に満たされる。
    • メモ：T-Varの前提は空の文脈では成立しない。導出木の一番下は $\vdash t : T$ であり、文脈は空である。型付け規則を下から上に読むと、T-Absのみが文脈に束縛を追加する。そのため、導出木でT-Varが使われているとしたら、それはT-Absより上にある。しかしT-Absでは、前提で性質を仮定せず、結論のみで性質を満たせる。したがって、T-Varの場合を示す必要はない。
• T-Absの場合、
  • 定理とT-Absの結論を以下のように対応付ける。
    • $t = \lambda x: T_1 . ~ t_2$
  • $t$ は値であるため性質を満たす。
• T-Appの場合、
  • 定理とT-Appの結論を以下のように対応付ける。
    • $\varnothing = \Gamma$
    • $t = t_1 ~ t_2$
  • T-Appの前提より、
    • $\vdash t_1 : T_{11} \rightarrow T_{12}$
  • 帰納法の仮定より、
    • $t_1$ は値であるか、ある $t'_1$ が存在して $t_1 \longrightarrow t'_1$
    • $t_2$ は値であるか、ある $t'_2$ が存在して $t_2 \longrightarrow t'_2$
  • $t_1$ が値の場合、
    • $t_2$ が値の場合、
      • $t_1$ が $T_{11} \rightarrow T_{12}$ 型の値であるため、標準形補題より $t_1 = \lambda x : T_{11} . ~ t_{12}$ である。
      • E-AppAbsにより $t = (\lambda x : T_{11} . ~ t_{12}) ~ t_2 \longrightarrow [x \mapsto t_2]t_{12} = t'$ と評価できる。
    • ある $t'_2$ が存在して $t_2 \longrightarrow t'_2$ である場合、E-App2により $t = t_1 ~ t_2 \longrightarrow t_1 ~ t'_2 = t'$ と評価できる。
  • ある $t'_1$ が存在して $t_1 \longrightarrow t'_1$ である場合、E-App1により $t = t_1 ~ t_2 \longrightarrow t'_1 ~ t_2 = t'$ と評価できる。
• T-Zeroの場合、
  • 定理とT-Zeroの結論を以下のように対応付ける。
    • $t = 0$
  • $t$ は値であるため性質を満たす。
• T-Succの場合、
  • 定理とT-Succの結論を以下のように対応付ける。
    • $t = \text{succ} ~ t_1$
  • T-Succの前提より、
    • $\vdash t_1 : \text{Nat}$
  • 帰納法の仮定より、
    • $t_1$ は値であるか、ある $t'_1$ が存在して $t_1 \longrightarrow t'_1$
  • $t_1$ が値の場合、 $t_1$ は $\text{Nat}$ 型の値であるから、標準形補題より $t_1$ は抽象構文にしたがった数値である。抽象構文の定義より $t = \text{succ} ~ t_1$ もまた数値であり、数値は値であるから性質を満たす。
  • ある $t'_1$ が存在して $t_1 \longrightarrow t'_1$ である場合、E-Succにより $t = \text{succ} ~ t_1 \longrightarrow \text{succ} ~ t'_1 = t'$ と評価できる。
• T-Letの場合、
  • 定理とT-Letの結論を以下のように対応付ける。
    • $t = (\text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2)$
  • 帰納法の仮定より、
    • $t_1$ は値であるか、ある $t'_1$ が存在して $t_1 \longrightarrow t'_1$
  • $t_1$ が値の場合、E-LetVにより $t = (\text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2) \longrightarrow [x \mapsto t_1]t_{2} = t'$ と評価できる。
  • ある $t'_1$ が存在して $t_1 \longrightarrow t'_1$ である場合、E-Letにより $t = (\text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2) \longrightarrow (\text{let} ~ x ~ \text{=} ~ t'_1 ~ \text{in} ~ t_2) = t'$ と評価できる。

$\Gamma \vdash t : T$ かつ、 $\Delta$ が $\Gamma$ の並べ替えならば、 $\Delta \vdash t : T$ である。さらに、前者と後者の導出の深さ（導出木の高さ）は同じ。

概要：文脈の要素を並べ替えても、その文脈のもとで型付けができる。

証明：

$\Gamma \vdash t : T$ の導出に関するごく簡単な構造的帰納法によって示す。

• T-Varの場合、
  • 文脈に関する暗黙の仮定より、変数名がそれぞれ異なる文脈を並べ替えたとしても $x : T \in \Delta$ が成り立つため、 T-Varより $\Delta \vdash x : T$ もまた成り立つ。
  • 並び替え前後で導出の深さは変化していない。
• T-Absの場合、
  • 帰納法の仮定より、 $\Delta , x : T_1 \vdash t_2 : T_2$ であるため、T-Absより $\Delta \vdash \lambda x: T_1 . ~ t_2 : T_1 \rightarrow T_2$ が成り立ち、これは所望の結論である。
    • 以降、同様の形式の議論について「帰納法の仮定とT-Xから、所望の結論が成り立つ」と表現する。
  • 並び替え前後で導出の深さは変化していない。
• T-Appの場合、
  • 帰納法の仮定とT-Appから、所望の結論が成り立つ
  • 並び替え前後で導出の深さは変化していない。
• T-Zeroの場合、
  • 前提がないため、T-Zeroにより即座に $\Delta \vdash 0 : \text{Nat}$ が成り立つ。
  • 並び替え前後で導出の深さは変化していない。
• T-Succの場合、
  • 帰納法の仮定とT-Succから、所望の結論が成り立つ
  • 並び替え前後で導出の深さは変化していない。
• T-Letの場合、
  • 帰納法の仮定とT-Letから、所望の結論が成り立つ
  • 並び替え前後で導出の深さは変化していない。

$\Gamma \vdash t : T$ かつ、 $x \notin dom(\Gamma)$ ならば、 $\Gamma , x : S \vdash t : T$ である。さらに、前者と後者で導出の深さ（導出木の高さ）は同じ。

概要：文脈に現れない変数の束縛を追加しても、その文脈のもとで型付けができる。

証明：

$\Gamma \vdash t : T$ の導出に関するごく簡単な構造的帰納法によって示す。

• T-Varの場合、
  • $x' \notin dom(\Gamma)$ である $x' : S$ を $\Gamma$ に追加したとしても、 $x : T \in \Gamma , x' : S$ であることは変わらないため、 T-Varより $\Gamma , x' : S \vdash x : T$ が成り立つ。
  • 束縛の追加前後で導出の深さは変化していない。
• T-Absの場合、
  • 帰納法の仮定より、$x' \notin dom(\Gamma)$ である $x' : S$ について、 $\Gamma , x : T_1 , x' : S \vdash t_2 : T_2$ である。T-Absより、 $\Gamma , x' : S \vdash \lambda x: T_1 . ~ t_2 : T_1 \rightarrow T_2$ が成り立ち、これは所望の結論である。
    • 以降、同様の議論について「帰納法の仮定とT-Xから、所望の結論が成り立つ」と表現する。
  • 束縛の追加前後で導出の深さは変化していない。
• T-Appの場合、
  • 帰納法の仮定とT-Appから、所望の結論が成り立つ。
  • 束縛の追加前後で導出の深さは変化していない。
• T-Zeroの場合、
  • 前提がないため、 $x' \notin dom(\Gamma)$ である $x' : S$ について、T-Zeroにより即座に $\Gamma , x' : S \vdash 0 : \text{Nat}$ が成り立つ。
  • 束縛の追加前後で導出の深さは変化していない。
• T-Succの場合、
  • 帰納法の仮定とT-Succから、所望の結論が成り立つ。
  • 束縛の追加前後で導出の深さは変化していない。
• T-Letの場合、
  • 帰納法の仮定とT-Letから、所望の結論が成り立つ。
  • 束縛の追加前後で導出の深さは変化していない。

$\Gamma , x : S \vdash t : T$ かつ、 $\Gamma \vdash s : S$ ならば、 $\Gamma \vdash [x \mapsto s]t : T$ である。

概要：型付けされた項 $t$ について、文脈中の任意の束縛 $x : S$ を取り出して、その束縛なしに $S$ 型が付く項 $s$ があるなら、$[x \mapsto s]t$ にも型が付く。

証明：

$\Gamma , x : S \vdash t : T$ の導出に関する構造的帰納法によって示す。

• T-Varの場合、
  • 補題とT-Varの結論を以下のように対応付ける。
    • $t = y$
  • 補題の1つ目の前提より
    • $\Gamma , x : S \vdash t : T$
    • $\Gamma , x : S \vdash y : T$
    • 逆転補題1によって、
    • $y : T \in \Gamma , x : S$
  • 補題のもう1つの前提より
    • $\Gamma \vdash s : S$
  • 所望の結論は、 $\Gamma \vdash [x \mapsto s]t : T$ である。代入の定義より、 $x = y$ と $x \ne y$ の場合を検証すれば十分である。
    • $x = y$ の場合、
      • $y : T \in \Gamma , x : S$ から $T = S$ である。
      • 所望の結論は
        • $\Gamma \vdash [x \mapsto s]t : T$
        • $\Gamma \vdash [x \mapsto s]y : T$
        • $\Gamma \vdash s : T$
        • $\Gamma \vdash s : S$
      • であり、これは補題の前提に含まれるため所望の性質を満たす。
    • $x \ne y$ の場合、
      • $y : T \in \Gamma , x : S$ について、 $x : S$ は $y$ と無関係の束縛のため、 $y : T \in \Gamma$ である。
      • 所望の結論は
        • $\Gamma \vdash [x \mapsto s]t : T$
        • $\Gamma \vdash [x \mapsto s]y : T$
        • $\Gamma \vdash y : T$
      • であり、これは $y : T \in \Gamma$ と T-Varより成り立つ。
• T-Absの場合、
  • 補題とT-Absの結論を以下のように対応付ける。
    • $\Gamma , x : S = \Delta$
    • $t = \lambda y: T_1 . ~ t_2$
      • ただし、 $y \ne x$ かつ $y \notin FV(s)$ かつ $y \notin dom(\Gamma)$ を仮定する （仮定1）
      • フレッシュな変数を選び、もとのラムダ抽象をα-変換することでこの仮定はいつでも満たせる。
    • $T = T_1 \rightarrow T_2$
  • T-Absの前提は
    • $\Delta , y : T_1 \vdash t_s : T_2$
    • $\Gamma , x : S , y : T_1 \vdash t_2 : T_2$
    • 並び替え補題より
    • $\Gamma , y : T_1 , x : S \vdash t_2 : T_2$ （1）
  • 補題の前提より、
    • $\Gamma \vdash s : S$
    • 弱化補題と仮定1より
    • $\Gamma , y : T_1 \vdash s : S$ （2）
  • 帰納法の仮定より、1と2に補題を適用して
    • $\Gamma , y : T_1 \vdash [x \mapsto s]t_2 : T_2$
    • T-Absより
    • $\Gamma \vdash \lambda y : T_1 . ~ [x \mapsto s]t_2 : T_1 \rightarrow T_2$
    • $\Gamma \vdash \lambda y : T_1 . ~ [x \mapsto s]t_2 : T$ （3）
  • 所望の結論は
    • $\Gamma \vdash [x \mapsto s]t : T$
    • $\Gamma \vdash [x \mapsto s](\lambda y: T_1 . ~ t_2) : T$
    • 代入の定義と仮定1より
    • $\Gamma \vdash \lambda y : T_1 . ~ [x \mapsto s]t_2 : T$ （3）
  • 3は型付けの前提、補題の前提および帰納法の仮定のみから得られるため、所望の結論は満たされる。
• T-Appの場合、
  • 補題とT-Appの結論を以下のように対応付ける。
    • $\Gamma , x : S = \Delta$
    • $t = t_1 ~ t_2$
    • $T = T_{12}$
  • T-Appの前提は
    • $\Gamma , x : S \vdash t_1 : T_{11} \rightarrow T_{12}$ （1）
    • $\Gamma , x : S \vdash t_2 : T_{11}$ （2）
  • 補題の前提より
    • $\Gamma \vdash s : S$ (3)
  • 帰納法の仮定より、補題を1と3に適用して
    • $\Gamma \vdash [x \mapsto s]t_1 : T_{11} \rightarrow T_{12}$ （4）
  • 帰納法の仮定より、補題を2と3に適用して
    • $\Gamma \vdash [x \mapsto s]t_2 : T_{11}$ （5）
  • 4、5とT-Appより
    • $\Gamma \vdash [x \mapsto s]t_1 ~ [x \mapsto s]t_2 : T_{12}$
    • $\Gamma \vdash [x \mapsto s]t_1 ~ [x \mapsto s]t_2 : T$
    • $\Gamma \vdash [x \mapsto s](t_1 ~ t_2) : T$
    • $\Gamma \vdash [x \mapsto s]t : T$
  • となるため、所望の結論が成り立つ。
• T-Zeroの場合、
  • 補題とT-Zeroの結論を以下のように対応付ける。
    • $\Gamma , x : S = \Delta$
    • $t = 0$
    • $T = \text{Nat}$
  • 所望の結論は
    • $\Gamma \vdash [x \mapsto s]t : T$
    • $\Gamma \vdash [x \mapsto s]0 : \text{Nat}$
    • $\Gamma \vdash 0 : \text{Nat}$
  • となり、T-Zeroより即座に成り立つ。
• T-Succの場合、
  • 補題とT-Succの結論を以下のように対応付ける。
    • $\Gamma , x : S = \Delta$
    • $t = \text{succ} ~ t_1$
    • $T = \text{Nat}$
  • T-Succの前提は
    • $\Delta \vdash t_1 : \text{Nat}$
    • $\Gamma , x : S \vdash t_1 : \text{Nat}$ （1）
  • 補題の前提より
    • $\Gamma \vdash s : S$ （2）
  • 帰納法の仮定より、1と2に補題を適用して
    • $\Gamma \vdash [x \mapsto S]t_1 : \text{Nat}$
    • T-Succより
    • $\Gamma \vdash \text{succ} ~ [x \mapsto S]t_1 : \text{Nat}$
    • $\Gamma \vdash [x \mapsto S](\text{succ} ~ t_1) : \text{Nat}$
    • $\Gamma \vdash [x \mapsto S]t : \text{Nat}$
    • $\Gamma \vdash [x \mapsto S]t : T$
  • となるため、所望の結論が成り立つ。
• T-Letの場合、
  • 補題とT-Letの結論を以下のように対応付ける。
    • $\Gamma , x : S = \Delta$
    • $t = (\text{let} ~ y ~ \text{=} ~ t_1 ~ \text{in} ~ t_2 : T_2)$
      • ただし、 $y \ne x$ かつ $y \notin FV(s)$ かつ $y \notin dom(\Gamma)$ を仮定する （仮定1）
      • フレッシュな変数を選び、 $t_2$ 内のもとの変数を置き換えることでこの仮定はいつでも満たせる。
    • $T = T_2$
  • T-Letの前提は
    • $\Gamma , x : S \vdash t_1 : T_1$ （1）
    • $\Gamma , x : S , y : T_1 \vdash t_2 : T_2$ （2）
  • 補題の前提より
    • $\Gamma \vdash s : S$ （3）
    • 弱化補題と仮定1より
    • $\Gamma , y : T_1 \vdash s : S$ （4）
  • 帰納法の仮定より、1と3に補題を適用して
    • $\Gamma \vdash [x \mapsto s]t_1 : T_1$ （5）
  • 2に並べ替え補題を適用して
    • $\Gamma , y : T_1 , x : S \vdash t_2 : T_2$
    • 帰納法の仮定より、4と補題を適用して
    • $\Gamma , y : T_1 \vdash [x \mapsto s]t_2 : T_2$ （6）
  • 5、6、T-Letより
    • $\Gamma \vdash \text{let} ~ y ~ \text{=} ~ [x \mapsto s]t_1 ~ \text{in} ~ [x \mapsto s]t_2 : T_2$
    • $\Gamma \vdash \text{let} ~ y ~ \text{=} ~ [x \mapsto s]t_1 ~ \text{in} ~ [x \mapsto s]t_2 : T$ （7）
  • 所望の結論は
    • $\Gamma \vdash [x \mapsto s]t : T$
    • $\Gamma \vdash [x \mapsto s](\text{let} ~ y ~ \text{=} ~ t_1 ~ \text{in} ~ t_2 : T_2) : T$
    • 代入の定義と仮定1より
    • $\Gamma \vdash \text{let} ~ y ~ \text{=} ~ [x \mapsto s]t_1 ~ \text{in} ~ [x \mapsto s]t_2 : T_2 : T$ （7）
  • 7は型付けの前提、補題の前提および帰納法の仮定のみから得られるため、所望の結論は満たされる。

$\Gamma \vdash t : T$ かつ $t \longrightarrow t'$ ならば $\Gamma \vdash t' : T$

概要：項を評価しても同じ型が付く。

証明：

$\Gamma \vdash t : T$ の導出に関する構造的帰納法によって示す。

• T-Varの場合、
  • 定理とT-Varの結論を以下のように対応付ける。
    • $t = x$
  • $t$ は変数であり、変数は評価できないため定理の前提を満たさない。したがって所望の結論は自明に満たされる。
• T-Absの場合、
  • 定理とT-Absの結論を以下のように対応付ける。
    • $t = \lambda x: T_1 . ~ t_2$
  • $t$ はラムダ抽象であり、ラムダ抽象は評価できないため定理の前提を満たさない。したがって所望の結論は自明に満たされる。
• T-Appの場合、
  • 定理とT-Appの結論を以下のように対応付ける。
    • $t = t_1 ~ t_2$
    • $T = T_{12}$
  • T-Appの前提より
    • $\Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$ （1）
    • $\Gamma \vdash t_2 : T_{11}$ （2）
  • 帰納法の仮定と1、2より
    • $t_1 \longrightarrow t'_1$
    • $\Gamma \vdash t'_1 : T_{11} \rightarrow T_{12}$ （3）
    • $t_2 \longrightarrow t'_2$
    • $\Gamma \vdash t'_2 : T_{11}$ （4）
  • 定理の前提より
    • $t \longrightarrow t'$ （5）
  • $t$ に適用されうる評価規則はE-App1、E-App2、E-AppAbsであるため、それぞれのケースを検証すれば十分である。
    • E-App1の場合、
      • 5とE-App1の結論を対応付けると
        • $t' = t'_1 ~ t_2$
      • 3と2、T-Appより
        • $\Gamma \vdash t'_1 ~ t_2 : T_{12}$
        • $\Gamma \vdash t'_1 ~ t_2 : T$
        • $\Gamma \vdash t' : T$
      • となるため、所望の結論を満たす。
    • E-App2の場合、
      • 5とE-App2の結論を対応付けると
        • $t' = t_1 ~ t'_2$
      • 1と4、T-Appより
        • $\Gamma \vdash t_1 ~ t'_2 : T_{12}$
        • $\Gamma \vdash t_1 ~ t'_2 : T$
        • $\Gamma \vdash t' : T$
      • となるため、所望の結論を満たす。
    • E-AppAbsの場合、
      • 5とE-AppApsの結論を対応付けると
        • $t_1 = \lambda x : T_{11} . ~ t_{12}$ （6）
        • $t' = [x \mapsto t_2]t_{12}$
      • 1より
        • $\Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$
        • 6より
        • $\Gamma \vdash \lambda x : T_{11} . ~ t_{12} : T_{11} \rightarrow T_{12}$
        • 逆転補題2より
        • $\Gamma , x : T_{11} \vdash t_{12} : T_{12}$
        • 2と代入補題より
        • $\Gamma \vdash [x \mapsto t_2]t_{12} : T_{12}$
        • $\Gamma \vdash t' : T_{12}$
        • $\Gamma \vdash t' : T$
      • となるため、所望の結論を満たす。
• T-Zeroの場合、
  • 定理とT-Zeroの結論を以下のように対応付ける。
    • $t = 0$
  • $t$ は0であり、0は評価できないため定理の前提を満たさない。したがって所望の結論は自明に満たされる。
• T-Succの場合、
  • 定理とT-Succの結論を以下のように対応付ける。
    • $t = \text{succ} ~ t_1$
    • $T = \text{Nat}$
  • T-Succの前提より
    • $\Gamma \vdash t_1 : \text{Nat}$ （1）
  • 帰納法の仮定と1より
    • $t_1 \longrightarrow t'_1$
    • $\Gamma \vdash t'_1 : \text{Nat}$ （2）
  • 定理の前提より
    • $t \longrightarrow t'$ （3）
  • $t$ に適用されうる評価規則はE-Succだけであるため、
    • $t' = \text{succ} ~ t'_1$
  • 2とT-Succより
    • $\Gamma \vdash \text{succ} ~ t'_1 : \text{Nat}$
    • $\Gamma \vdash t' : \text{Nat}$
    • $\Gamma \vdash t' : T$
  • となるため、所望の結論を満たす。
• T-Letの場合、
  • 定理とT-Succの結論を以下のように対応付ける。
    • $t = (\text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2)$
    • $T = T_2$
  • T−Letの前提より
    • $\Gamma \vdash t_1 : T_1$ （1）
    • $\Gamma , x : T_1 \vdash t_2 : T_2$ （2）
  • 帰納法の仮定と1、2より
    • $t_1 \longrightarrow t'_1$
    • $\Gamma \vdash t'_1 : T_1$ （3）
    • $t_2 \longrightarrow t'_2$
    • $\Gamma , x : T_1 \vdash t'_2 : T_2$ （4）
  • 定理の前提より
    • $t \longrightarrow t'$ （5）
  • $t$ に適用されうる評価規則はE-Let、E-LetVであるため、それぞれのケースを検証すれば十分である。
    • E-Letの場合、
      • 5とE-Letの結論を対応付けると
        • $t' = (\text{let} ~ x ~ \text{=} ~ t'_1 ~ \text{in} ~ t_2)$
      • 3と2、T-Letより
        • $\Gamma \vdash \text{let} ~ x ~ \text{=} ~ t'_1 ~ \text{in} ~ t_2 : T_2$
        • $\Gamma \vdash t' : T_2$
        • $\Gamma \vdash t' : T$
      • となるため、所望の結論を満たす。
    • E-LetVの場合、
      • 5とE-LetVの結論を対応付けると
        • $t' = [x \mapsto t_1]t_2$
      • 2より
        • $\Gamma , x : T_1 \vdash t_2 : T_2$
        • 1と代入補題より
        • $\Gamma \vdash [x \mapsto t_1]t_2 : T_2$
        • $\Gamma \vdash t' : T_2$
        • $\Gamma \vdash t' : T$
      • となるため、所望の結論を満たす。

$\vdash t : T$ かつ $t \longrightarrow^\ast t' \nrightarrow$ ならば $t'$ は値である。

概要：空の文脈で型が付いた $t$ を評価していって停止するなら、それは値である。

証明：

$t \longrightarrow^\ast t'$ の評価の長さ $n$ による数学的帰納法によって示す。

• $n = 0$ の場合、
  • 定理の1つ目の前提より
    • $\vdash t : T$
  • これと進行定理より
    • $t$ は値であるか、ある $t'$ が存在して $t \longrightarrow t'$
  • しかし、定理のもう1つの前提より
    • $t \longrightarrow^0 t' \nrightarrow$
    • つまり
    • $t \nrightarrow$
  • したがって $t$ は値であり、所望の結論を満たす。
• 任意の $n$ について定理を仮定し、 $n + 1$ について示す。
  • 定理の前提より
    • $\vdash t : T$ （1）
    • $t \longrightarrow^{n + 1} t' \nrightarrow$ （2）
  • $t$ の1ステップ評価結果を $u$ とおくと
    • $t \longrightarrow u$ （3）
    • $u \longrightarrow^n t' \nrightarrow$ （4）
  • 保存定理を1と3に適用して
    • $\vdash u : T$ （5）
  • 帰納法の仮定より、定理を5と4に適用すると、 $t'$ は値であり、所望の結論を満たす。

任意の型代入 $\sigma$ について、$\Gamma \vdash t : T$ ならば $\sigma \Gamma \vdash \sigma t : \sigma T$ である。

概要：型代入を適用しても型付けは保存される

証明：

$\Gamma \vdash t : T$ の導出に関する構造的帰納法による。

• T-Varの場合、
  • 定理とT-Varの結論を以下のように対応付ける。
    • $t = x$ （1）
  • 定理の前提より
    • $\Gamma \vdash t : T$
    • 1より
    • $\Gamma \vdash x : T$
    • 逆転補題1より
    • $x : T \in \Gamma$
    • 文脈に対する型代入の定義より
    • $x : \sigma T \in \sigma \Gamma$
    • T-Varより
    • $\sigma \Gamma \vdash x : \sigma T$
    • 変数に対する型代入の定義より
    • $\sigma \Gamma \vdash \sigma x : \sigma T$
    • 1より
    • $\sigma \Gamma \vdash \sigma t : \sigma T$
  • したがって、所望の性質を満たす。
• T-Absの場合、
  • 定理とT-Absの結論を以下のように対応付ける。
    • $t = \lambda x : T_1 . ~ t_2$ （1）
    • $T = T_1 \rightarrow T_2$ （2）
  • 定理の前提より
    • $\Gamma \vdash t : T$
    • 1と2より
    • $\Gamma \vdash \lambda x : T_1 . ~ t_2 : T_1 \rightarrow T_2$
    • 逆転補題2より
    • $\Gamma , x : T_1 \vdash t_2 : T_2$
    • 帰納法の仮定より
    • $\sigma (\Gamma , x : T_1) \vdash \sigma t_2 : \sigma T_2$
    • $\sigma \Gamma , x : \sigma T_1 \vdash \sigma t_2 : \sigma T_2$
    • T-Absより
    • $\sigma \Gamma \vdash \lambda x : \sigma T_1 . ~ \sigma t_2 : \sigma T_1 \rightarrow \sigma T_2$
    • $\sigma \Gamma \vdash \sigma (\lambda x : T_1 . ~ t_2) : \sigma T_1 \rightarrow \sigma T_2$
    • 2より
    • $\sigma \Gamma \vdash \sigma t : \sigma T_1 \rightarrow \sigma T_2$
    • $\sigma \Gamma \vdash \sigma t : \sigma (T_1 \rightarrow T_2)$
    • 1より
    • $\sigma \Gamma \vdash \sigma t : \sigma T$
  • したがって、所望の性質を満たす。
• T-Appの場合、
  • 定理とT-Appの結論を以下のように対応付ける。
    • $t = t_1 ~ t_2$ （1）
    • $T = T_{12}$ （2）
  • 定理の前提より
    • $\Gamma \vdash t : T$
    • 1と2より
    • $\Gamma \vdash t_1 ~ t_2 : T_{12}$ （3）
  • 3と逆転補題3より
    • $\Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$
    • 帰納法の仮定より
    • $\sigma \Gamma \vdash \sigma t_1 : \sigma (T_{11} \rightarrow T_{12})$
    • $\sigma \Gamma \vdash \sigma t_1 : \sigma T_{11} \rightarrow \sigma T_{12}$ （4）
  • 3と逆転補題3より
    • $\Gamma \vdash t_2 : T_{11}$
    • 帰納法の仮定より
    • $\sigma \Gamma \vdash \sigma t_2 : \sigma T_{11}$ （5）
  • 4、5とT-Appより
    • $\sigma \Gamma \vdash \sigma t_1 ~ \sigma t_2 : \sigma T_{12}$
    • $\sigma \Gamma \vdash \sigma (t_1 ~ t_2) : \sigma T_{12}$
    • 1より
    • $\sigma \Gamma \vdash \sigma t : \sigma T_{12}$
    • 2より
    • $\sigma \Gamma \vdash \sigma t : \sigma T$
  • したがって、所望の性質を満たす。
• T-Zeroの場合、
  • 定理とT-Appの結論を以下のように対応付ける。
    • $t = 0$ （1）
    • $T = \text{Nat}$ （2）
  • T-Zeroより
    • $\sigma \Gamma \vdash 0 : \text{Nat}$
    • $0$ に対する型代入の定義より
    • $\sigma \Gamma \vdash \sigma 0 : \text{Nat}$
    • $\text{Nat}$ に対する型代入の定義より
    • $\sigma \Gamma \vdash \sigma 0 : \sigma \text{Nat}$
    • 1と2より
    • $\sigma \Gamma \vdash \sigma t : \sigma T$
  • したがって、所望の性質を満たす。
• T-Succの場合、
  • 定理とT-Succの結論を以下のように対応付ける。
    • $t = \text{succ} ~ t_1$ （1）
    • $T = \text{Nat}$ （2）
  • 定理の前提より
    • $\Gamma \vdash t : T$
    • 1と2より
    • $\Gamma \vdash \text{succ} ~ t_1 : \text{Nat}$
    • 逆転補題5より
    • $\Gamma \vdash t_1 : \text{Nat}$
    • 帰納法の仮定より
    • $\sigma \Gamma \vdash \sigma t_1 : \sigma \text{Nat}$
    • T-Succより
    • $\sigma \Gamma \vdash \text{succ} ~ (\sigma t_1) : \sigma \text{Nat}$
    • $\sigma \Gamma \vdash \sigma (\text{succ} ~ t_1) : \sigma \text{Nat}$
    • 1より
    • $\sigma \Gamma \vdash \sigma t : \sigma \text{Nat}$
    • 2より
    • $\sigma \Gamma \vdash \sigma t : \sigma T$
  • したがって、所望の性質を満たす。
• T-Letの場合、
  • 定理とT-Letの結論を以下のように対応付ける。
    • $t = (\text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2)$ （1）
    • $T = T_2$ （2）
  • 定理の前提より
    • $\Gamma \vdash t : T$
    • 1と2より
    • $\Gamma \vdash \text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2 : T_2$ （3）
  • 3と逆転補題6より
    • $\Gamma \vdash t_1 : T_1$
    • 帰納法の仮定より
    • $\sigma \Gamma \vdash \sigma t_1 : \sigma T_1$ （4）
  • 3と逆転補題6より
    • $\Gamma , x : T_1 \vdash t_2 : T_2$
    • 帰納法の仮定より
    • $\sigma (\Gamma , x : T_1) \vdash \sigma t_2 : \sigma T_2$
    • $\sigma \Gamma , x : \sigma T_1 \vdash \sigma t_2 : \sigma T_2$ （5）
  • 4、5とT-Letより
    • $\sigma \Gamma \vdash \text{let} ~ x ~ \text{=} ~ \sigma t_1 ~ \text{in} ~ \sigma t_2 : \sigma T_2$
    • $\sigma \Gamma \vdash \sigma (\text{let} ~ x ~ \text{=} ~ t_1 ~ \text{in} ~ t_2) : \sigma T_2$
    • 1より
    • $\sigma \Gamma \vdash \sigma t : \sigma T_2$
    • 2より
    • $\sigma \Gamma \vdash \sigma t : \sigma T$
  • したがって、所望の性質を満たす。