定理証明(theorem proving)とは、プログラミングにおける次世代のテスト・開発手法である。
たとえば、プログラムで1からnまでの整数の和を計算するにはどうすればいいだろうか。for文? 再帰? いやいや、足し算が許されるのは小学生までだよね。当然、等差数列の和の公式 n * (n + 1) / 2 でしょう。
ところで、上記の計算は実際には1からnまでの整数を「足して」いないわけであるが、本当に大丈夫だろうか。もちろん、賢明な読者の皆様であれば等差数列の和の公式の証明が容易に頭に浮かぶに違いない。
しかし、もっと複雑なケースになるとどうだろうか。証明を思いつくだろうか。思いついた証明は本当に正しいだろうか。ちょっと本格的にプログラミングをかじった人なら、ユニットテストをきちんと書けば問題ないと言うだろう。しかし、本当にテストケースにないケースまで大丈夫と言い切れるだろうか。
そこで出てきた考え方が定理証明である。目標とする仕様を「数学の定理」として証明すれば、テストケースを選ばずともすべての場合について仕様を満たすことが保証できるのである。
実際にはどのようにして開発を行うかというと、
という手順になる。ユニットテストから始める開発をテスト駆動開発というのに対して、定理証明から始まる開発なので証明駆動開発という。
残念ながら2.のプロセスが自動化されていないために難易度が高く、Coq, Agdaなどの定理証明器があるものの、現実にはほとんど実用化には至っておらず、重要な中核部分に限定的に使われる程度にとどまっている。
上記の証明駆動開発で最も成果をあげている定理証明器がCoqである。
Coq自体はプログラミング言語ではなく、記述に用いられるプログラミング言語はGallinaというものである。定理証明器プログラム自体はOCamlでプログラミングされている。
証明できた場合は、そこからHaskell, OCaml, Schemeのソースコードに変換できる。数学的な証明なので、数学的な意味での関数を扱う関数型言語と相性がいいようである。
主な実績として、4色問題の証明(2004年: なお、4色問題自体が最初に証明されたのは1976年のことである)や、コンパイラが最適化処理しても動作内容が変わらないことが定理証明で保証されたCコンパイラCompCertの開発などがある。
定理証明で証明されるのは、「引数がある条件を満たすとき、引数を受け取った関数の戻り値が別の条件を満たす」ということである。単純な例を挙げると「引数が自然数だったら、引数を足し合わせる関数の戻り値は自然数」とか、「引数が整数なら、引数で除算を行う関数の戻り値は有理数である」といった感じである。
もう少しプログラミングを意識した例を挙げるなら「引数も戻り値もnullではない」とか「戻り値の配列の長さが10以上なので、配列の10番目の要素にアクセスする関数に戻り値を引数として渡すことができる」といったことである。冒頭の例に立ち返るなら「引数が自然数の時、戻り値は1から引数までの整数を足し合わせたものに等しい」といったものも当てはまる。CompCertの例をとれば「引数などの環境が同じであれば、最適化しないコードの実行結果と、コンパイラが最適化したコードの実行結果は必ず常に同じである」ということになる。
いずれにしても「証明」である以上、数学・論理学上の命題の形をとるので、要件を命題に置き換える作業が必要になる。もし命題に変換する際に何か勘違いしてしまったら、いくらコーディングにバグがなくても台無しになってしまう。定理証明といえども残念ながらそこまで保証することはできない。ユニットテストでも同様の問題を抱えてはいるが、網羅性の限界が自明なユニットテストに対し、定理証明が完璧性を求めて行われることを考えると、命題の選択は完璧性を損ないうる危険なポイントといえるかもしれない。
整数を扱う場合は理論とコンピューター上の計算が一致するので定理証明しやすいが、それでもコンピューターで扱える整数の上限を超えてしまう場合などはうまくいかない可能性がある。
また、浮動小数点数ではコンピューターでは常に丸め誤差の問題がついてまわるので、ぴったり理論通りに計算されない可能性が高くなる。
一方で圏論由来のモナドのようなジェネリクスを用いた高階関数の動作検証は、引数や戻り値の型の検証のみがなされ、実際に数値計算が行われることはないので、理論とプログラムが一致しやすいといえる。
掲示板
掲示板に書き込みがありません。
急上昇ワード改
最終更新:2024/04/18(木) 16:00
最終更新:2024/04/18(木) 16:00
ウォッチリストに追加しました!
すでにウォッチリストに
入っています。
追加に失敗しました。
ほめた!
ほめるを取消しました。
ほめるに失敗しました。
ほめるの取消しに失敗しました。