型なしの算術式と型付きの算術式を例に、計算がどのように体系付けられていくのか、その流れの一例をみていきます。これによりプログラミング言語の基本的な側面を形式的に取り扱うことができます。

ちなみにこの記事は型システム入門とプログラム意味論という本を参考にして書いてます。厳密でないところや間違ったところがたくさんあると思いますが、気になる箇所はこちらの本をあたると良いと思います。間違いなどはこっそりコメントを頂けたりすると嬉しいです。

言語構文の定義付けについて考える

次のように、真理値 true, false、条件式、数値定数 0、後者関数 succ、前者関数 pred、ゼロ判定の演算子 iszero の簡単な構文からなる小さな言語を考えてみましょう。

項 t ::= true | false | if t then t else t | 0 | succ t | pred t | iszero t

これと同じことを次のように帰納的な形で定義することもできます。

[帰納的な項の定義] 項の集合とは以下の条件を満たす最小の集合 T である
(1) {true, false, 0} ∈ T
(2) t ∈ T ならば {succ t, iszero t} ⊆ T
(3) t ∈ T かつ u ∈ T かつ v ∈ T ならば if t then u else v ∈ T

また以下のように推論規則による定義の仕方もあります。

[推論規則による項の定義] 項の集合は次の規則によって定義される 　この推論規則は、上段を前提として下段を導けるというものです。とくに上段がない、つまり前提を必要としない規則のことを特に公理と呼びます。また以下のように項の要素を生成する具体的手続きを書き下すことによる定義の仕方もあります。

[具体的な項の定義] 自然数 i について、集合 T_i、 項の集合 T をそれぞれ以下のように定義する。

項の評価について考える

以上のように色々な方法で言語の構文を定式化できました。さてプログラミング言語を考えるときには各項がどのように評価されるということも考えなければなりません。この評価がどのようにされるかという議論を意味論と呼びます。意味論の形式化にも様々なバリエーションがあります。

さて、手始めにブール値の評価について考えてみましょう。すると次の３つの評価関係が成り立つと一般的な言語機能として良さそうだということはなんとなく分かるかと思います。

(1) if true then t else u → t | t, u ∈ T
(2) if false then t else u → u | t, u ∈ T
(3) t → t' => if t then u else v → if t' then u else v | t, u, v ∈ T

このように項の状態に対して遷移規則を定めることにより、項の評価を定義していく方法を操作的意味論と言います（そのなかでもスモールステップ意味論というスタイルになります）。なお表記の都合上、推論規則は (上段) => (下段) という書き方をしています。

この３つの規則が何を言っているのかと同じくらい、何を言っていないのかということも重要です。たとえばこれらの規則から「if 全体が評価される前に then 節や else 節が評価されることはない」という評価戦略が読み取れます。

この３つの評価関係から例えば if false then false else true という項は、(2) を適用して true という値に評価することができます。true はこれ以上適用できる規則がありません。このような項を正規形と呼びます。

評価できない項

ブール値の評価について定めましたが数値についてはまだでした。まとめて評価規則を定義しましょう。まずは構文と値の再確認をしておきます。

[構文]
項 t ::= true | false | if t then t else t | 0 | succ t | pred t | iszero t

[値]
値　 v ::= true | false | nv
数値 nv ::= 0 | succ nv

つづいて評価規則についてみてみます。

[評価規則 t → t']　(t, t', u, v ∈ T)
(1) if true then t else u → t
(2) if false then t else u → u
(3) t → t' => if t then u else v → if t' then u else v
(4) t → t' => succ t → succ t'
(5) => pred 0 → 0
(6) => pred (succ nv) → nv
(7) t → t' => pred t → pred t'
(8) => iszero 0 → true
(9) => iszero (succ nv) → false
(10) t → t' => iszero t -> iszero t'

このように言語の操作的意味論を形式化すると、例えば succ true のようにこれ以上評価できない、つまり正規形であるが、値ではないというようなパターンが生まれてしまいます。こういうような項を行き詰まり状態と呼びます。

プログラミング言語の機能としてこの行き詰まり状態をどう扱うかということはひとつ大きな課題となります。エラーを表す新しい項を導入したり、型を導入してこの手のエラーを予め防ぐなどいくつかのアプローチがあります。

型の導入による行き詰まり状態の回避の試み

項を実際には評価せずとも succ true のような行き詰まり状態にならないことが分かると便利です。このような仕組みのひとつとして型を導入することを考えましょう。前述の言語では、値として数値とブール値を扱っていたためそれらに対応する型 Nat と Bool を導入します。

[型付け規則 t:T (T = Bool | Nat) ]
(a) true: Bool
(b) false: Bool
(c) t: Bool, u: T, v: T => if t then u else v: T
(d) => 0: Nat
(e) t: Nat => succ t: Nat
(f) t: Nat => pred t: Nat
(g) t: Nat => iszero t: Bool

以上のような型付け規則により、項 t が評価したときにある型の値になることを静的に、つまり評価することなく判断することができるようになります。項 t に対してある型 T が存在して、t: T となるとき t は型付け可能と言います。

安全性を支える型システム

行き詰まり状態を回避する手段のひとつとして型を導入したことからも何となく分かるように、型システムの最も基本的な性質は「安全性」です。正しく型付けされた項は行き詰まり状態にならない「安全性」は少し難しい話になりますが、型の進行定理と保存定理というものによって保証されます。証明はしませんが、それぞれ以下のような内容になります。

[評価規則 t → t']　(t, t', u, v ∈ T)
(1) if true then t else u → t
(2) if false then t else u → u
(3) t → t' => if t then u else v → if t' then u else v
(4) t → t' => succ t → succ t'
(5) => pred 0 → 0
(6) => pred (succ nv) → nv
(7) t → t' => pred t → pred t'
(8) => iszero 0 → true
(9) => iszero (succ nv) → false
(10) t → t' => iszero t -> iszero t'

これら２つの定理によって、正しく型付けされた項は最終的に値として評価でき、行き詰まり状態に陥らないということがわかります。