このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

「プログラミング = 証明」のはずだが

カリー/ハワード/ランベック対応の話を何度かしました。「カリー/ハワード/ランベック対応の辞書」の最後に、最近のカリー/ハワード/ランベック対応関連の記事をまとめてあります。最近に限らないなら:

さて、カリー/ハワード/ランベック対応によれば、“関数型プログラミング言語でプログラミングをすること”と、“形式化された証明記述言語で証明を書くこと”は同じことです。しかし実際には:

  • 「俺はプログラムなら書けるが、証明を書ける気がしない」
  • 「証明はある程度書けるつもりだが、プログラミングとなるとカラッキシいかんわ」

といったことが多いかと思います。これはなぜでしょう? すぐ思いつく当然な理由は:

  • 関数型プログラミングと形式的証明では、記述言語や背景理論で使っている用語や記号があまりにも違うので、翻訳が難しい。

カリー/ハワード/ランベック対応は、型付きラムダ計算(関数型プログラミングの原型)と論理の対応を与えるので、翻訳のガイドラインにはなります。実際、用語の対応表をまとめたのが「カリー/ハワード/ランベック対応の辞書」と関連記事達です。

自然言語の翻訳(例えば日本語とフランス語)でも言えることですが、辞書と文法があれば翻訳が出来るかというと、そうではありません。文化や習慣の違いがあります。意訳をしたり、説明を付け足したり、場合によっては翻訳語を造語する必要もあります。

プログラミングと論理でも文化や習慣の違い(大きな違い)があります。興味の対象や価値観も違うのです。用語や記号を翻訳しようとしても、翻訳先に適切な対応物がなかったりします。あるいは、ほぼ同じ意味の用語・記号を割り当てても、用語・記号の運用法が違うので齟齬が生じたり。難しい*1

それと、証明ソフトウェアによる証明記述ではまた別な問題があります。現在主流の証明記述法はタクティクを使うものです。タクティクは証明ソフトウェアに与えるコマンドです。タクティク・スクリプトを“証明”と呼びますが、これは、我々が常識的に想定する証明とはまったく違うものです。

タクティク・スクリプトは、(常識的な意味の)証明ではなくて、ソフトウェアに証明を生成させるためのコマンド(それがタクティク)を並べたものです。タクティク・スクリプトをタクティク・インタープリタ(実行系)が実行すると、内部的に証明*2が生成されます。

論理や証明論を勉強して*3、形式化された証明を自在に書けるようになった人でも、タクティク・スクリプトは書けません。タクティク・スクリプトを「証明だ」と見せられたら困惑するでしょう。

タクティクは対話的環境で実行できるので、タクティク・スクリプトとしての証明の記述は一種のゲームとして遂行できます(「Coqの証明ゲームの表側と裏側 (誰も書かないCoq入門以前 4)」参照)。証明ソフトウェアによる証明ゲームの達人が、論理や証明論を理解しているとも限りません。証明ゲームはトレーニングと慣れで上達しますから。

タクティク証明の困った問題点は、独特なコマンド言語で書かれているので「普通の人はもとより、論理・証明論のエキスパートでさえ読めない」ことです。コマンド言語に慣れて読めるようになっても、解釈はタクティク・インタープリタの実行を頭のなかでシミュレートすることになります。タクティク・インタープリタはバックワード・リーズニングだけを実行するので人間の思考過程とは食い違います*4。(バックワード・リーズニングについては次の記事参照。)

カリー/ハワード/ランベック対応によれば、「関数型プログラム←→直接証明(タクティク証明ではない)」と対応します。直接証明とは、タクティクを使わずに、人間がラムダ式を使って書く証明です。現在の証明ソフトウェアでも直接証明は書けますが、タクティク証明に比べるとサポートが非常に薄い。その結果、ソフトウェア支援が得られるタクティク証明に流れ、直接証明を書く人が減る -- みんな使わないから直接証明サポートは不要 ‥‥ という悪循環で直接証明は冷遇されているのでしょう*5

「プログラミング = 証明」がリアリティを持つには、プログラミングと論理のあいだの、文化・習慣と言語運用まで含めた相互翻訳が確立されて、人間の思考過程を素直に表現する直接証明に対するソフトウェア支援が充実する必要があります。

*1:と書いていて、戸田奈津子さんはすごい人だ、と思いました。

*2:ここの「証明」は、常識的な証明に対応するラムダ式のことです。証明項とか証明オブジェクトとも呼ばれます。

*3:証明論は論理の一分野です。「論理の一般的知識、さらには証明論まで勉強して」という意味合いです。

*4:困った問題点があってもタクティク証明が主流なのは、短いスクリプトでコンパクトに書けて、アルゴリズム化がしやすく、自動証明にも容易に繋がるからです。

*5:MizarやIsabell/Isarは、人間可読な直接証明記述を目指したソフトウェアです。Isabell Isar のブログ内検索結果 参照。タクティク証明に比べて、直接証明のソフトウェア支援は設計・実装が困難という事情もあって、主流になれないのでしょう。