Types and Programming Languages/8章 型付き算術式
8.1. 型
算術式の構文は
$ \begin{array}{rl} \mathtt{項\ t ::=} & \\ & \mathtt{true} \mid \mathtt{false} \mid 0 \\ & \mathtt{if\ t\ then\ t\ else\ t} \\ & \mathtt{succ\ t} \mid \mathtt{pred\ t}\mid \mathtt{iszero\ t} \\ \mathtt{値\ v ::=} &\\ &\mathtt{true} \mid \mathtt{false} \mid \mathtt{nv} \\ \mathtt{数値\ nv ::=} &\\& \mathtt{0} \mid \mathtt{succ\ nv} \end{array}
となっており、項の評価を進めると値になるか、評価規則を適用できないが値でもない行き詰まり状態になる。
行き詰まり状態とは、間違った実装のプログラムに相当する。これを実行せずに行き詰まり状態にならないことを検査したい。
いま、数値と真偽値を区別するために2つの型 $ \mathtt{Nat} と $ \mathtt{Bool}を追加する。
$ \begin{array}{rl} 型\ \mathtt{S}, \mathtt{T}, \mathtt{\dots ::=} &\\ & \mathtt{Nat} \mid \mathtt{Bool} \end{array}
項$ \mathtt{t}が型$ \mathtt{T}を持つとは、$ \mathtt{t}を評価すると明らかに、つまり静的に$ \mathtt{T}型の値になることを指す。
改めて、型は保守的に付けられ、if true then 0 else false のような項は行き詰まりにならないが、ここで定義する型では分類することができないため、このプログラムは静的にrejectされる。
8.2. 型付け関係
型付け関係は $ \mathtt{t} : \mathtt{T}と書き表し、項に型を割り当てる以下の6つの推論規則から成る集合によって定義される。
$ \mathtt{true} : \mathtt{Bool}\ \left(\mathrm{T-True}\right)\quad \mathtt{false} : \mathtt{Bool}\ \left(\mathrm{T-False}\right) \quad \dfrac{\mathtt{t_1} : \mathtt{Bool} \quad \mathtt{t_2} : \mathtt{T} \quad \mathtt{t_3}: \mathtt{T}}{\mathtt{if\ t_1\ then\ t_2\ else\ t_3} : \mathtt{T} }\ \left(\mathrm{T-If}\right)
$ \mathtt{0}:\mathtt{Nat}\ \left(\mathrm{T-Zero}\right) \quad \dfrac{\mathtt{t_1}:\mathtt{Nat}}{\mathtt{succ\ t_1}: \mathtt{Nat}}\ \left(\mathrm{T-Succ}\right) \quad \dfrac{\mathtt{t_1}:\mathtt{Nat}}{\mathtt{pred\ t_1}: \mathtt{Nat}}\ \left(\mathtt{T-Pred}\right)
$ \dfrac{\mathtt{t}: \mathtt{Nat} }{\mathtt{iszero\ t} : \mathtt{Bool}}\ \left(\mathrm{T-IsZero}\right)
定数 true, false を Bool 型に含めている。
T-If 規則をみてみると、 then節とelse節の型が同じT型であることを要求しており、式全体の型は T となる。
数値も同様に、 0 を Nat 型に含め、 succ と pred も Nat を受け取って Nat を返す型となっている。
iszero は Nat をうけとって Bool を返すような型である。
定義 8.2.1.
算術式における型付け関係 $ \left(:\right) は項と型の二項関係であり、型付け規則の全てのインスタンスを満たす最小の関係である。項 $ \mathtt{t}に対して、ある型$ \mathtt{T}が存在して $ \mathtt{t}:\mathtt{T}となるとき、 $ \mathtt{t}は型付け可能(または正しく型付けされている)という。 $ \square
補題 8.2.2. 型付け関係の逆転
1. $ \mathtt{true} : \mathtt{R}ならば$ \mathtt{R}=\mathtt{Bool}である。
2. $ \mathtt{false} : \mathtt{R}ならば$ \mathtt{R}=\mathtt{Bool}である。
3. $ \mathtt{if\ t_1\ then\ t_2\ else\ t_3} : \mathtt{R}ならば、$ \mathtt{t_1}: \mathtt{Bool}かつ$ \mathtt{t_2}: \mathtt{R}かつ$ \mathtt{t_3} : \mathtt{R}である。
4. $ \mathtt{0}:\mathtt{R}ならば$ \mathtt{R} = \mathtt{Nat}である。
5. $ \mathtt{succ\ t}:\mathtt{R}ならば、$ \mathtt{t}:\mathtt{Nat}かつ$ \mathtt{R}=\mathtt{Nat}である。
6. $ \mathtt{pred\ t}:\mathtt{R}ならば、$ \mathtt{t}:\mathtt{Nat}かつ$ \mathtt{R}=\mathtt{Nat}である。
7. $ \mathtt{iszero\ t}:\mathtt{R}ならば、$ \mathtt{t}:\mathtt{Nat}かつ$ \mathtt{R}=\mathtt{Nat}である。
$ \square
証明 8.2.2.
型付け関係の定義により直ちに成り立つ。
1. T-True より 1. が成り立つ。
2. T-False より 2. が成り立つ。
3. ......(後略) $ \square
逆転補題は、与えられた妥当な型付けの判別式からその証明がどのように生成されたかを示すため、生成補題とも呼ばれる。逆転補題から項の型を計算する再帰アルゴリズムを直接得られる。なぜなら、各項の構文形式の型を、部分項の型からどのように計算するかを述べているからである。
例えば 補題 8.2.2. の 3. を例に取ると、ある if 式の型は部分項の t_2 の型かつ t_3 の型であることが分かる。
演習 8.2.3.
正しく型付けされた項のすべての部分項は、正しく型付けされていることを証明せよ。
評価導出と同様に、型付け導出も型付け規則のインスタンスの木である。以下は if iszero 0 then 0 else pred 0 : Nat の型付け判断式のための導出木である。
$ \dfrac{ \dfrac{\dfrac{}{\mathtt{0}: \mathtt{Nat}^{\mathrm{T-Zero}} } }{\mathtt{iszero\ 0}: \mathtt{Bool}^{\mathrm{T-IsZero}}} \quad \dfrac{}{\mathtt{0}: \mathtt{Nat}^{\mathrm{T-Zero}}} \quad \dfrac{ \dfrac{}{\mathtt{0}:\mathtt{Nat}^{\mathrm{T-Zero}}} } {\mathtt{pred\ 0}: \mathtt{Nat}^{\mathrm{T-Pred}} } }{\mathtt{if\ iszero\ 0\ then\ 0\ else\ pred\ 0} : \mathtt{Nat}^{\mathrm{T-If}}}
型付け判断式はプログラムの型に対する形式的な主張、型付け規則は型付け判断式の間の含意、そして型付け導出は型付け規則に基づいた演繹である。
定理 8.2.4. 型の一意性
各項 $ \mathtt{t}は高々一つの型を持つ。つまり、もし $ \mathtt{t}が型付け可能ならば、その型は一意である。さらに、上記の推論規則から構築される型付け導出はたった1つだけである。 $ \square
高々一つとは、$ \mathtt{t}が最大で一つの型を持つ(型がつかないか、一意な型がつく)ことを指している。
証明 8.2.4.
$ \mathtt{t}に関する構造的帰納法で、それぞれの場合に逆転補題(+帰納法の仮定)を適用すればよい。
型のついた項 $ \mathtt{t}: \mathtt{T}に対し、
1. $ \mathtt{t} = \mathtt{true}のとき、
逆転補題より $ \mathtt{T}=\mathtt{Bool}であり、他に型付け規則はない。
2. $ \mathtt{t} = \mathtt{false}のとき、
3. $ \mathtt{t} = \mathtt{if\ t_1\ then\ t_2\ else\ t_3}のとき、
逆転補題により $ \mathtt{t_1}:\mathtt{Bool}である。
定理 8.2.4. が成り立つと仮定すると、逆転補題より $ \mathtt{t_2}: \mathtt{T}かつ$ \mathtt{t_3}:\mathtt{T}となり、他に型付け規則はない。
5. $ \mathtt{t}=\mathtt{succ\ t_1}のとき、
$ \mathrm{\left(T-Succ\right)} に関する逆転補題により、 $ \mathtt{t_1} : \mathtt{Nat} かつ $ \mathtt{T} = \mathtt{Nat}となり、$ \mathtt{succ\ t_1}に対する 型付け規則は $ \mathrm{\left(T-Succ\right)}を除いて他にない。
型付き算術式は1つの項は高々1つの型を持つが、部分型付けなどでは、項は複数の型を持ちうる。
8.3. 安全性=進行+保存
あらゆる型システムの最も基本的な性質は、安全性(健全性とも呼ぶ)である。
この性質は、正しく型付けされた項は"おかしく"なることがないことを示している。
プログラムが"おかしく"なるとはどういう状態かを定めたので、続いて、正しく型付けされた項は行き詰まり状態にならないことを示す。
これは、進行定理と保存定理という2つの定理によって示すことができる。
進行定理 (progress)
正しく型付けされた項は行き詰まり状態ではなく、値であるか、いずれかの評価規則を適用できる。
保存定理 (preservation)
正しく型付けされた項が評価できるならば、評価後の項もまた正しく型付けができる。
進行定理の証明のために、BoolとNat型の標準形を定める。
補題 8.3.1. 標準型
1. v が Bool 型ならば、 v は true または false である。
2. v が Nat 型ならば、 v は nv に属する。$ \square
証明
1. について、算術式の文法により、値は true, false, 0, succ nv (ただし nv は数値)である。最初の2つは直ちに主張を満たす。逆転補題により、 0 と succ nv は Nat 型を持ち、型の一意性により Bool 型を持たないため、 1. が成り立つ。 2. も同様。$ \square
定理 8.3.2. 進行
t を正しく型付けされた項 (つまりある T について t : T となる t) と仮定する。このとき t は値であるか、 ある t' が存在して t → t' となる。$ \square
証明
t : T の導出に関する帰納法による。 $ \mathrm{T-True}、$ \mathrm{T-False}、$ \mathrm{T-Zero} の場合は t が値であることから成立する。それ以外の場合に関して議論していく。
$ \square
定理 8.3.3. 保存
t : T かつ t → t' ならば、 t' : T となる。$ \square
証明
t : T の導出に関する帰納法による。すべての部分導出に関して保存定理が成り立つと仮定し、導出の最後の規則適用部分に関して場合分けを行い証明をすすめる。$ \square
演習 8.3.4.
保存定理を評価導出に関する帰納法を用いて証明せよ。$ \square
保存定理はしばしば主部簡約または主部評価と呼ばれる。
型の一意性に関しては、部分型などが挙げられるように、それを満たさない型システムが存在する。しかし、進行と保存は全ての型システムが満たすべき基本的な性質である。Javaの操作的意味論を小ステップで形式化すると型保存性が壊れるが大ステップならOKらしい。
演習 8.3.5.
評価規則 $ \mathrm{E-PredZero} は特に 0 に適用する場合直観に反する。この規則を1ステップ評価の定義から取り除くことで納得感のある動作を達成できるだろうか。
演習 8.3.6.
主部簡約の性質を見ていると、反対に主部を展開するような性質もなりたつ可能性を感じる。 t → t' かつ t' : T なら t : T は常に成り立つだろうか。成り立つ場合には証明、または反例を挙げよ。
演習 8.3.8.
行き詰まりの状態を評価すると wrong という状態に簡約する規則を追加した評価関係を仮定すると、このときの型安全性はどのように形式化すべきか。