定理証明系

院生時代に ML 上の HOL を触ったのが最初ですが、あまりピン来ず。だいたい、

＊　証明できました

ぐらいしか返してこないし。他の人がいろいろいじっているのを見たこともあるのだけど、難しいんだよね。テストとかモデル検証とかは、実行してデバッグに近いのでわかりやすいんだけど。

学部時代には、ちゃんと Natural deduction 習ったし、いろいろやったんだけどなぁ。去年辺りは、sequent calculus の方も見たし。でも、論文とか見て間違い探しみたいなのができるほどでもなく。

プログラミングと一階述語論理は、ほぼ同じものなので、本来なら証明ベースでプログラミングするものだろうと思うのだが、数年前のモデル検証のワークショップでは、

＊　証明を組み上げる方法はダメだ (だからモデル検証)

みたいな大きな声で主張している人たちがいたし。

まぁ、たしかに、証明できるプログラムの大きさは数千行まで来ていて、証明された OS のコードとかもあるんだけど、なにせ、それが論文になるくらいだからね。そもそも、

＊　何に対して証明するか

ってのが問題になっていて、それは Property とか呼ばれるプログラムが満たすべき性質なんだけど、それをどうやってそろえるかもよくわかっていないところがある。それはテストに近いものですが「止まらない」とか「均等に要求を拾う」とかのテストしづらいものも入っている。残念ながら、必要十分な Property をそろえることは不可能だろうと僕も思う…　大きさの問題を除いても難しいです。

でも、だから、証明系のアプローチがダメだとは思わない。小さい部分にはもちろん有効だし、デバッグ/テスト/モデル検証は当てづっぽなところがあるからな。それに、「どうして動くのか」を理解するためには証明が必須だから。

Lamport も自分の分散アルゴリズムの正しさを示すために、自前の証明系を持っていたし。それが使いやすいかどうかはともかく、そういう方法を持っているということは重要だと思う。

理論系の論文だと「この推論規則と公理系は自動証明系でチェックした」とか書いてあったりするしな。

今時だと、Coq かなぁ。 Kindle 上の Interactive Theorem Proving and Program Development: Cql'Art: The Calculus of Indective Constructions が、電子書籍にしては、超汚くてがっかりです。これだったら紙の方がまし。