定理証明とは (テイリショウメイとは) [単語記事]

定理証明(theorem proving)とは、プログラミングにおける次世代のテスト・開発手法である。

概要

たとえば、プログラムで1からnまでの整数の和を計算するにはどうすればいいだろうか。for文? 再帰? いやいや、足し算が許されるのは小学生までだよね。当然、等差数列の和の公式 n * (n + 1) / 2 でしょう。

ところで、上記の計算は実際には1からnまでの整数を「足して」いないわけであるが、本当に大丈夫だろうか。もちろん、賢明な読者の皆様であれば等差数列の和の公式の証明が容易に頭に浮かぶに違いない。

しかし、もっと複雑なケースになるとどうだろうか。証明を思いつくだろうか。思いついた証明は本当に正しいだろうか。ちょっと本格的にプログラミングをかじった人なら、ユニットテストをきちんと書けば問題ないと言うだろう。しかし、本当にテストケースにないケースまで大丈夫と言い切れるだろうか。

そこで出てきた考え方が定理証明である。目標とする仕様を「数学の定理」として証明すれば、テストケースを選ばずともすべての場合について仕様を満たすことが保証できるのである。

証明駆動開発

実際にはどのようにして開発を行うかというと、

仕様をコードで書く
1.を定理と考え、その証明をコードで書く
2.の証明を定理証明器というプログラムにかけて、証明が正しいか検証する。
3.で証明が正しければ、その証明を別のプログラミング言語のソースコードに変換する。
4.のソースコードをコンパイル・実行する。
5.が正しく動作することは数学的に保証されている(もっとも、定理証明器とコンパイラにバグがなければだが)。

という手順になる。ユニットテストから始める開発をテスト駆動開発というのに対して、定理証明から始まる開発なので証明駆動開発という。

残念ながら2.のプロセスが自動化されていないために難易度が高く、Coq, Agdaなどの定理証明器があるものの、現実にはほとんど実用化には至っておらず、重要な中核部分に限定的に使われる程度にとどまっている。

Coq

上記の証明駆動開発で最も成果をあげている定理証明器がCoqである。

Coq自体はプログラミング言語ではなく、記述に用いられるプログラミング言語はGallinaというものである。定理証明器プログラム自体はOCamlでプログラミングされている。

証明できた場合は、そこからHaskell, OCaml, Schemeのソースコードに変換できる。数学的な証明なので、数学的な意味での関数を扱う関数型言語と相性がいいようである。

主な実績として、4色問題の証明(2004年: なお、4色問題自体が最初に証明されたのは1976年のことである)や、コンパイラが最適化処理しても動作内容が変わらないことが定理証明で保証されたCコンパイラCompCertの開発などがある。

「何が」証明されるのか

定理証明で証明されるのは、「引数がある条件を満たすとき、引数を受け取った関数の戻り値が別の条件を満たす」ということである。単純な例を挙げると「引数が自然数だったら、引数を足し合わせる関数の戻り値は自然数」とか、「引数が整数なら、引数で除算を行う関数の戻り値は有理数である」といった感じである。

もう少しプログラミングを意識した例を挙げるなら「引数も戻り値もnullではない」とか「戻り値の配列の長さが10以上なので、配列の10番目の要素にアクセスする関数に戻り値を引数として渡すことができる」といったことである。冒頭の例に立ち返るなら「引数が自然数の時、戻り値は1から引数までの整数を足し合わせたものに等しい」といったものも当てはまる。CompCertの例をとれば「引数などの環境が同じであれば、最適化しないコードの実行結果と、コンパイラが最適化したコードの実行結果は必ず常に同じである」ということになる。

いずれにしても「証明」である以上、数学・論理学上の命題の形をとるので、要件を命題に置き換える作業が必要になる。もし命題に変換する際に何か勘違いしてしまったら、いくらコーディングにバグがなくても台無しになってしまう。定理証明といえども残念ながらそこまで保証することはできない。ユニットテストでも同様の問題を抱えてはいるが、網羅性の限界が自明なユニットテストに対し、定理証明が完璧性を求めて行われることを考えると、命題の選択はミスが起こりうる危険なポイントといえるかもしれない。