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

Proof Assistantは大体次のいずれかの方式をとるものが多いです。

• 適当なロジックの適当な公理系の証明を解釈するもの: 数学がやっている証明の形式化をそのままやるやり方です。IsabelleやHOLなど。

• Curry-Howard対応を用いるもの: 要は型付きラムダ計算を直接実装するやり方です。CoqやAgdaなど。

どっちでも構いませんがどっちを選ぶかによって実装は割と変わってきます。今回はIsabelleと同じく前者の方法をとります。

ところで、Proof Assistant(言語)には大きく分けると次の2種類の言語を持ちます。

• 命題記述言語: これは命題を記述する言語というだけでなく、Proof Assistantに組み込まれているロジックそのものを表現するために必要な言語でもあります。

• 証明記述言語: 証明を記述するためには専用の言語が必要な場合があります。ラムダ計算を直接実装する場合はラムダ項そのものでも別に構いません(Agdaみたいな)が、証明を記述するためにメタ言語を載せている言語も(Coqとか)あります。あるいはproverを実装するならこの言語から呼び出せるようにします。

Isabelleの場合は、前者がPure logicと呼ばれるロジックで、後者はIsarが該当します。

証明の記述にはいくつかのやり方があります。ラムダ計算を実装する場合はラムダ項を直接書くようにするのが楽ですが、公理系を実装する場合は真面目に作る必要があります。

雰囲気としては、次のような操作で記述できるとよさそうです。 (インタラクティブに書けるならこんな感じという気持ちですが、普通にファイルに記述してチェッカーを走らせる場合も裏ではこういう感じになっています)

1. Proof Assistantを起動する

2. 証明したい命題を入力 (例: a -> a)

3. 現在のゴールが a -> a になる

4. 証明を記述する (例: \x. x や apply Identity のように入力する)

5. 証明が完了する

証明を書くにはゴールをユーザーに表示し続ける仕組みはあったほうがよくて、ただまぁそれを真面目にやろうとするとエディタ・プラグインの開発が必要になるのでインタラクティブシェルみたいなものを作るのがとりあえず無難かなという気がします。

proof assistantに備わっている命題記述言語はIsabelleでいうところのPure logicと言いましたが、これは組み込みのロジックなだけでユーザーが証明を書くのにこの言語しか選択肢がないわけではありません。ロジックとは記号からなる項とその上の規則がいくつかあれば実装可能なので、組み込みのロジックを用いて新たに(ライブラリとして)別のロジックを実装することが出来ます。 このようにして組み込みのロジックで新たに別のロジックを実装するのは、ちょうどIsabelleもPure logicの上でHOLやFOLをライブラリとして提供しているのと同じです。このようにする利点として、組み込みのロジックはcheckerやproverにとって都合の良いロジックを選び、ユーザーに記述させるロジックはより読み書きしやすいものを選ぶ、みたいなことが出来ます。

ここでライブラリで定義されているロジックに対して組み込みのロジックをメタロジックと呼ぶことにします。

当然ながらメタロジックが弱すぎると欲しいロジックが定義できなかったりするのでそのへんは注意が必要です。まともに数学をしたいならfirst-order logicくらいは欲しくなるという気がします(がもっと弱くしてもいいのかもしれません、ロジック詳しくないのでよくわかりません)。

公理系を用いた証明は、公理・推論規則をゴールに適用していくことで記述するわけです。しかしそれだけでは通常不便なので色々便利なコマンドを作ったりproverを作ったりすることになると思います。

ところでこういう証明用のコマンドを実装するためにマクロとかそういうものが欲しくなると思います。 ここではコマンドは推論規則の列を、つまり証明を生成するマクロとして登録しておくことにします。例えばCoqではLtacという専用のマクロ記述言語(と呼んでいいのかな？普通に証明生成言語と呼ぶべきかもしれません)がありますが、IsabelleではSMLで内部実装のAPIを呼び出してこういう感じのことをしています。

マクロ記述用の言語も本当は用意するべきですが今回は面倒なのでやりません。 proof assistantの実装をHaskellでやるので、マクロもHaskellで記述したものを起動時に読み込むことで対処します。

proof assistantの実装の雰囲気がなんとなく伝わりつつあるでしょうか。

実装の詳細についての説明は次回に回します。