ニコニコ大百科モバイル

7/2(月)よりスマホまたはPCでアクセスした場合、各デバイス向けのサイトへ自動で転送致します


定理証明


ヨミ: テイリショウメイ

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


概要


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

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

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

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


証明駆動開発


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

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

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

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


Coq


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

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

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

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


「何が」証明されるのか


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

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

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


相性


整数を扱う場合は理論コンピューター上の計算が一致するので定理証明しやすいが、それでもコンピューターで扱える整数の上限をえてしまう場合などはうまくいかない可性がある。

また、浮動小数点数ではコンピューターでは常に丸め誤差の問題がついてまわるので、ぴったり理論通りに計算されない可性が高くなる。

一方で圏論由来のモナドのようなジェネリクスを用いた高階関数の動作検証は、引数や戻り値の検証のみがなされ、実際に数値計算が行われることはないので、理論プログラムが一致しやすいといえる。


関連動画



■sm1276083[ニコ動]


関連項目



関連リンク



最終更新日: 16/02/24 05:42
タグ検索 パソコン版を見る


[0]TOP
ニコニコ動画モバイル
運営元:ドワンゴ