定理証明

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

概要

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

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

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

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

証明駆動開発

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

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

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

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

Coq

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

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

証明できた場合は、そこからHaskell, OCaml, Schemeのソースコードに変換できる。

数学的な証明なので、数学的な意味での関数を扱う関数型言語と相性がいいようである。

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

関連動画

関連項目

• 定理
• 関数
• ユニットテスト
• 関数型言語
• プログラミング関連用語の一覧