| Edit this page | Report an issue |
これまでに実装したインタプリタは，与えられたプログラムを，セマンティクスにしたがって評価することにより実行結果を得ていた．例えば，実装したインタプリタを使って式3+5を評価すると8が評価結果として返ってくる．式let x = 2 in x + 3を評価すると5が評価結果として返ってくる．
一方で，このインタプリタは評価するプログラムによっては実行時に型エラーを起こして落ちてしまうことがある．例えば，3 4 は関数ではない値 3 を適用しようとしていて実行時型エラーを起こすし（実際に評価してみよう），let f x = x + 1 in f true も実行時型エラーを起こす（実際に試してみよう）．
実行時型エラーは結構困りものである．以下の例を見てみよう．
let rec f x n =
if n <= 0 then 3 4 (* (A) *)
else
let x = (* めっちゃ重い計算 *)
f x (n + -1)
in
f 0 1000000003 4 を評価しようとしましたが，3 は関数ではありません．落ちます．このような悲劇を防ぐ方法はあるだろうか．まず繰り返し回数を減らしてテストをせよ，というアドバイスはもっともだが，締め切り1日前の午前3:00には冷静にテストをできないかもしれない．そんな締切ギリギリになって実験をするのが悪いというアドバイスももっともだが，そんなシチュエーションになったことが無い者のみが石を投げなさい．
もし，このプログラムを 実行することなく (* (A) *)の場所に型エラーの可能性があることが分かるとしたらどうだろうか．プログラムを走らせようとすると，処理系が自動的に (* (A) *)のところに型エラーがあるから走らせられませんねえと知らせてくれる．これを修正して走らせれば（プログラムの修正に1分くらいかかって，走らせ始めるのが 3:01 くらいになるかもしれないが）次の日に無事論文に新しい実験結果が載せられるだろう．
しかし，プログラムを実行させずにプログラムの実行結果についての情報を得ることが本当に可能だろうか．実は，すでに皆さんはその技術を使っている．先程のプログラムを，めっちゃ重い計算ではないがもう少し軽い計算を繰り返すプログラムにしてみて，繰り返しのたびにメッセージを出力するようにして，ocaml に食べさせてみよう．
let rec f x n =
if n <= 0 then 3 4 (* (A) *)
else
let x = x mod 2 in
Format.printf "Hoge.@\n";
f x (n + -1)
in
f 0 100000000> ocaml
OCaml version 4.06.1
...
# let rec f x n =
if n <= 0 then 3 4 (* (A) *)
else
let x = x mod 2 in
Format.printf "Hoge.@\n";
f x (n + -1)
in
f 0 100000000;;
Error: This expression has type int
This is not a function; it cannot be applied.
ここまでの演習をやった人であれば，このエラーメッセージを何度も見たことだろう．だが，ここで注目すべきはエラーメッセージではなく，Hoge.という文字列が出力されていないことである．もしプログラムが実行された上で型エラーが検出されたのならば，この文字列が1億回出力されているはずである．つまり，ocamlは， プログラムを実行することなく，型エラーが存在する可能性を指摘している．
静的プログラム検証 (static program verification) は，プログラムを実行することなく，その内容を解析し，何らかの性質（ここでは実行時に型エラーが起こり得ないこと）が満たされているかどうかを検査する手法である．静的プログラム検証静的・動的についての注は，検証に用いる手法の正しさが数学的に厳密に証明されているときに 形式検証 (formal verification) と呼ばれる．名称についての注
静的・動的:「静的検証」の「静的」は “static” の訳で，プログラムの実行時の情報（例えば，プログラムの実行途中での環境の内容等）を用いず，実行前に得られる情報のみを用いるという意味である．対比される言葉に「動的検査」がある．これはプログラムの実行途中に行う検査で，例えば実行時型検査（実行時に関数適用を行う前に，関数として扱われるべき値が実際に関数であるかの検査等）やテスト，プロファイリングなどはこれに類する．なお，「静的検証」と「動的検査」は，どちらが優れているというものではない．というのは，「静的検査」によって何らかの性質を保証する問題は，大体の性質では決定不能（任意のプログラムを扱うことのできる，与えられた性質が成り立つかどうかについて，必ず正しい結果を出力して停止する検証アルゴリズムが存在しない）になってしまうからである．したがって，静的検査では，扱えるプログラムの種類を限定したり，検証手続きの停止性を諦めたり，出力された結果の正しさを一部諦めたり（具体的には，「バグがあるかも」と判断されても，実際にはバグがない可能性を許す）する必要がある．したがって，静的検証を用いる場合にも，動的検査と組み合わせて使う必要がある．
名称について: 「形式」は，多分 “formal” の訳で，「これでただしいんじゃん？」という感じで適当に（”informal” に）検証をするのではなく，数学的に検証手法の正しさを証明しましょう，という気持ちがこもっている．似た言葉として 形式手法 (formal method) という言葉を聞くことがあるかもしれない．これは，上記の意味でのプログラムの正しさの検証のみならず，ソフトウェア設計やテストケース設計などのソフトウェア開発一般に数学を使う手法で，形式検証はその意味で形式手法の一分野である．なお，同様の意味で 静的解析 (static analysis) と言うと，静的検証の一手法である 抽象解釈 (abstract interpretation) を使ったプログラム検証を指すことがある．（用語が混乱していて分かりにくい．僕も困っている．）
本章では，これまでに実装した MiniML 処理系に，静的検証の一種である 静的型推論 (static type inference) を実装する．OCaml でプログラムを書くと自動で型を推論してくれて，型エラーがあれば知らせてくれるアレである．型推論はプログラム中の式が（評価が停止するならば）どのような値を返すかを プログラムを実行することなく 解析するので静的検証の一種である．また，プログラムが 実行時に型エラーを起こさない ことを証明するための手法であるため，形式検証と言える．
本章では，これまでに実装した言語のための型推論を解説する．まず MiniML2 のための型推論からはじめて，徐々に言語を拡張しつつ，拡張された言語機能のための型推論を行う方法を解説する．