Proof Assistantを作る・理論編 その2

これは一人Computer Scienceアドベントカレンダー 17日目の記事です。

昨日に引き続き、Proof Assistantを作る話をしていきます。

今日は実際にこの後作っていくProof Assistant固有の話をしていきます。

Claire言語とその設計

唐突ですがこれから作るProof Assistantを「Claire1」と呼ぶことにします。

リポジトリ: myuon/claire

Claireは実際には複数の言語の組み合わせでできています:

  • FOL: Pure logicとしてはfirst-order logicを採用します。

  • LK: Proof SystemとしてはLK(Sequent Calculus)を採用します

  • Claire: Proof Assistant Claireの証明記述用の言語の名前です

  • コマンド記述言語(コマンド定義マクロ): コマンド記述言語はコマンド名からLKの規則の列を生成するものです。今回はHaskellで記述できるようにします。

  • HOLライブラリ: Isabelleと同じく、HOLをライブラリとして実装することが出来ます。することができるというだけでかなり大変なのでしませんが。

LKについて

Proof Systemとして、Sequent Calculus LKを採用します。定義はwikipediaのページでも見るといいんじゃないでしょうか。

The system LK - Wikipedia

今回LKを採用した理由として、natural deductionに比べると推論規則を適用した時のゴールの変形の選択肢が少ない(規則を適用する時に必要な情報が少ない)ことがあります。 というか、natural deductionは命題変数の数を減らすelimination ruleを多く含みますがelimination ruleはゴールに対して適用する、つまり下から上に読むと新たな変数を導入することになるので曖昧さが出やすいです。

それに比べるとSequent Calculusは(仮定とゴールを上手く用意することで)ruleが基本的にintro ruleばかりなので曖昧さが出にくいので、コマンドを適用して証明を書くのには便利かなと思って採用しました。

あとLK触れたことないのでちょっと触ってみたかった的なアレもあります(こっちの理由のほうが大きいかもしれない)。

LKについてそこまで説明をするつもりはありませんが、次のようなことをおさえておいてください。

  • judgementは Pn,P(n-1)..P1 |- Q1,Q2..Qm の形(PやQはfirst-order logicの論理式)。左側を仮定、右側を命題(propositions)という。

  • 仮定は「全てがなりたつ」 命題は「いずれかが成り立つ」の意味になる

  • 仮定は右から、命題は左から順番に読んでいく(まぁこれは記法の問題なのでどちらでもよいが)

  • 論理結合子に対する規則は、それが左辺に現れる場合と右辺に現れる場合とあることに注意。例えばAndの規則はAndL1, AndL2, AndRの3つ。

  • LKは古典的(背理法が使える)である。(注:命題の数を常に1つだけに制限すると直観主義になる)

  • (例) AndLの規則により B |- Qs ==> And(A,B) |- Qs がわかる。これは、「Bの下でQ1..Qmのいずれかが成り立つならばAかつBの元でもQ1..Qmのいずれかが成り立つ」という風に読むとよい。

  • (例) ImpLの規則により |- A,Qs ==> B |- Qs ==> Imp(A,B) |- Qs がわかる。これは、「AならばB」が「not AまたはB」と同値であることを使うと、「AまたはQsのいずれかが成り立ち、BのもとでQsのいずれかが成り立つならば、(not AまたはB)のもとではQsのいずれかが成り立つ」と読める。

まぁ意味がちゃんとわからなくとも、「LKはこういう(ゴールを変形してゆく)ルールからなります」「LKは"いい感じの"systemなので証明が書けます」くらいのノリでもいいです。

Claireのコマンドについて

Claireは(基本的には)コマンドを適用して、ゴールをどんどん変形していく感じになります。

ところでゴールへの変形というのは(当然)自由にやっていいわけではなく、基本的に適用できるルールはLKのルールだけです。 しかしそうすると例えば「すでに示した定理を再利用する」みたいなコマンドもないので大変不便です。

「すでに示した定理を新たに仮定に追加するコマンド use」を使ってよいかというのは、useを使って得られた証明図から、useを使わずに同じ論理式を示す証明図があることから保証されます。

まぁこういう感じで、アグレッシブに(LKのルール以外の方法で)ゴールを書き換えるコマンドを実装してもよいかどうかはその都度考える必要がありますので要注意です。

実装にあたって

さて次回からはいよいよHaskellコードの解説になります。

色々誤解があるといけないので事前に諸注意(言い訳)を述べておきます。

  • Proof Assitantとして特に独自性があるわけではない(基本的にはIsabelleの下位互換、jEditを使わなくてよいところだけが唯一の利点)

  • proverは実装しない(証明を生成する便利コマンドの類はいくつか実装します)

  • unifierは実装しない(曖昧さのある論理式の適用とか、subtermをいい感じに探して適用みたいな器用なことはできません)

  • マクロで定義されたコマンドのsyntaxがひどい(context-dependentなparser書くのつらそうだからやりたくなかった)

  • 標準ライブラリとしてHOLを提供といいつつHigher-order logic自体は実装できてない(全部やるとつらすぎる)

  • 洒落にならないくらい遅い(真面目な実装をサボりHaskellのインタープリターを実行時に呼び出すという荒業をしているため)

まぁそれでもコードは意外と面白い感じになっていると思います(希望的観測)。

まとめ

というわけでまた明日。

1

読みなんて適当でいいんですが個人的にはクレールと読んでいます。Isabelleがフランスの女性名らしいので同じくフランスの女性名から選びました。