Prologで証明アシスタント

を作ろう

h_sakurai

証明アシスタントとは?

人が与えられた規則の中から1つの規則を選んで計算を進めることで結果を導く過程を書き、その証明をコンピュータで整合性を検査するプログラムです。

例えば、1+2+3=6という計算のインタプリタを書けば計算できますが、それは自動的に証明してくれていることになります。

命題 1+2+3=6

証明 1+2=3で、3+3=6だから、1+2+3=6になる。□

というような話をプログラムで処理できるものです。

四則演算のインタプリタ

インタプリタを書いてみましょう。

eval(I1 = I1) :- integer(I1).

eval(E1 + E2 = I3) :- eval(E1 = I1), eval(E2 = I2), I3 is I1 + I2.

:- eval(1+2+3=6), halt.

これは自動的に計算出来るプログラムです。自動証明されます。

名前をつけよう

証明するにはどの述語を呼ぶのか分かるようにするために名前をつける必要があるでしょう。名前を付けてみます。

eval(I1 = I1):eint :- integer(I1).

eval(E1 + E2 = I3):eadd :- eval(E1 = I1):_, eval(E2 = I2):_, I3 is I1 + I2.

:- eval(1+2+3=R):_, writeln(R), halt.

名前を渡さないと動かないようになりました。

これを証明から使いたい。

証明木のイメージ

eval(1+2+3=6):eadd :-
(eval(1+2=3):eadd :-
(eval(1=1):eint:-integer(1)),
(eval(2=2):eint:-integer(2)),
3 is 1 + 2),
(eval(3=3):eint:-integer(3)),
6 is 3 + 3.

こんな感じに書きたい。 :-の後ろになぜそうなったかを書けるようにする。

証明木のイメージ

短い例だと

eval(1+2=3):eadd :-
(eval(1=1):eint:-integer(1)),
(eval(2=2):eint:-integer(1)),
(3 is 1 + 2).

eval(1=1):eint :- integer(1).

などと書きたい。でも、Prologにそんな機能はありません。

じゃあ、どうしよう???

そうだ!

処理系作ろう!

処理系を作ることを考える。

theorem(eval(I1 = I1):eint :- integer(I1)).
theorem((eval(E1 + E2 = I3):eadd :- eval(E1 = I1), eval(E2 = I2), I3 is I1 + I2)).
:- proof((
eval(1+2=3):eadd :-
(eval(1=1):eint:-integer(1)),
(eval(2=2):eint:-integer(2)),
(3 is 1 + 2))).
:- proof(eval(1=1):eint :- integer(1)).

などと書ける処理系を作ればいいんでないの?
Coqっぽいし方向性はあっているはず!

proof/1を考える。

proof(A : N :- Bs) :- theorem(A : N :- Bs).

みたいなイメージです。 でもBsはネストしてproofを呼ぶ必要がある。A:Nはまとめてよさそうです。

maptpl2(F,(A,As),(B,Bs)):- call(F,(A,B)), maptpl2(F,As,Bs).
maptpl2(F,A,B) :- call(F,(A,B)).
proof(A :- Bs) :- theorem(A :- Cs), maptpl2(proof1, Bs, Cs).

maptpl2は2つのタプルをmapする述語。
proofは定理を取り出して、前提条件をmaptpl2でproof1を呼び出します。

proof1/1を考える。

proof1/1は証明する項と定理をまとめて呼び出されるので例えば以下のような呼び出しになります:

proof1((eval(1=1):eint:-integer(1)),eval(I=I)))

これを処理するには以下のようにすればよいでしょう:

proof1(((A:N:-Bs),A)) :-proof(A:N:-Bs).

proof1((integer(1),integer(I)))のような場合は:-がないので、integer(1)=integer(I)と単一化してinteger/1を呼べばいいので、以下のようにすればよいでしょう:

proof1((A,A)) :- proof(A).
proof(A) :- call(A).

前提のない定理

theorem(oreha(jaiyan):gakidaisyo).みたいなのがあった場合前提条件なくても動かしたいです。

proof(A) :- theorem(A).
proof1((A:N,A)):- proof(A:N).

も追加しましょう。エラー対策に以下のものを書いておくとよいでしょう:

proof1((A,B)) :- writeln('proof error unmatch':(A,B)), fail.

なんかできた気がします。

こんなんで動くのか???

Demo

自動証明で失敗する問題

subtype(S, U) :- subtype(S,T),subtype(T,U).

subtype(a,b).

subtype(b,c).

:- subtype(a,c).

は左再帰があるので、無限ループしてしまうので自動証明に失敗する。
これを手動で解いてみよう。

abortをつけると便利

theorem(_:abort).

という定理を作ると便利です。

1+2+3を証明してみましょう。

:- proof((
eval(1+2+3=6):abort
)).

abortを使うと証明を省略することが出来ます。

線形論理型言語

  • prove/1
    • 式1つを受け取ってprove/3を呼ぶ
  • prove/3
    • メインの評価規則が並んでいる。
  • subcontext/2
    • eraseの評価に使う。
    • 線形論理の!以外はすべて消すのでPrologのCut的なもののようだ。
  • pick/3
  • pick_S/2
  • rule/1
Prologで証明アシスタントを作ろう - Google Slides