これは「Egison Advent Calendar 2019 - Qiita」の5日目の記事です。
はじめに
1年くらい前に「Egisonで定理証明なんて無謀っすよ。」
とか書いていたと思うけど、できるかもしれない。
『定理証明手習い』を参考にします。方法は以下です。
命題に対して、項書き換えを繰り返して、最終的にTrueにする
シンタックス
※Egisonの新しいシンタックスで書いています。
$ egison -N
で使えます。
あと、個人的なシンタックスハイライトの関係で、
ファイルの拡張子を勝手に.eginsにしています。本来は.egiです。
Inductive data
証明する命題を、EgisonのInductive dataで表現します。
EgisonのInductive dataは大文字始まりで、パターンマッチ時には、同名の小文字始まりになります。
マッチャーを定義します。再帰的な定義ができます。
nat := algebraicDataMatcher | o | s nat | x | add nat nat bool := algebraicDataMatcher | falsee | trueee | eqn nat nat expr := algebraicDataMatcher | ifte bool expr expr | b bool
注意点があります。
これはあくまでマッチャーで、パターンマッチ時に使うものです。
EgisonではInductive dataを使う前に、定義をおこなう必要はありません。
使いたい所で、例えばS (S (S O))などと書けば良いです。
実装
今回は、例題として、自然数の『n + 0 = n』を証明しようと思います。
数学での証明は、例えば以下のようになると思います。
n=0のとき n + 0 = n は 0 + 0 = 0 となるので、命題は成り立つ。 n=kで命題が成り立つと仮定すると、 k + 0 = k 両辺に1を加える (k+1) + 0 = (k+1) となるので、n=k+1の時も成り立つ。 よって、数学的帰納法により、命題は成り立つ。
本方式では、元の命題は
B (Eqn (Add X O) X)
となり、帰納法を適用した命題は
Ifte (Eqn X O)
(B (Eqn (Add X O) X))
(Ifte (Eqn (Add X O) X)
(B (Eqn (Add (S X) O) (S X)))
(B Trueee) )
となります。
書き換えたい所まで潜っていって、その場所で書き換える様に実装します。
equalSameを例に解説します。
Eqn x xをTrueeeに書き換えます。
equalSame n e := match e as expr with | ifte $b $t $f -> Ifte b (equalSame n t) (equalSame n f) | b $b -> B (equalSameBool n b) equalSameBool n b := match b as bool with | eqn #n #n -> Trueee | $z -> z
exprやboolは、上でalgebraicDataMatcherで定義したマッチャーです。
小文字始まりコンストラクタ名で、Inductive dataにマッチします。
その後は、$xでxに値を束縛します。
#xでxの値に一致するものにマッチします。
あとは->の右側でInductive dataを書き換えれば良いです。
各コマンド
書き換えをおこなう関数を、本稿では「コマンド」と呼ぶ事にします。
帰納法コマンドinductionはベタ書きです。今回の命題でしか動きません。
equalIfN,equalSame,ifSameは、『定理証明手習い』でも公理として書かれているものです。
equalIfNはIfte (Eqn x y)のthen部で、xをyに書き換えるコマンドです。
equalSameはEqn x xをTrueeeに書き換えるコマンドです。
ifSameはIfte b x xをxに書き換えるコマンドです。
実行結果
順に実行してみます。
> loadFile "prover1.egins" > input B (Eqn (Add X O) X) > induction input Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B (Eqn (Add (S X) O) (S X))) (B Trueee)) > add1Step (induction input) Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B (Eqn ★(S (Add X O)) (S X))) (B Trueee)) > equalIfN (Add X O) X (add1Step (induction input)) Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B (Eqn (S ★X) (S X))) (B Trueee)) > equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))) Ifte (Eqn X O) (B (Eqn (Add X O) X)) (Ifte (Eqn (Add X O) X) (B ★Trueee) (B Trueee)) > ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))) Ifte (Eqn X O) (B (Eqn (Add X O) X)) ★(B Trueee) > equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))) Ifte (Eqn X O) (B (Eqn (Add ★O O) ★O)) (B Trueee) > add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))) Ifte (Eqn X O) (B (Eqn ★O O)) (B Trueee) > equalSame O (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input))))))) Ifte (Eqn X O) (B ★Trueee) (B Trueee) > ifSame (Eqn X O) (B Trueee) (equalSame O (add1Step (equalIfN X O (ifSame (Eqn (Add X O) X) (B Trueee) (equalSame (S X) (equalIfN (Add X O) X (add1Step (induction input)))))))) B Trueee
うまくいっていますね。
一連のコマンドを適用する関数proofを作って、見やすくしましょう。
proof x fs := match fs as list something with | [] -> x | $f :: $fss -> proof (f x) fss
> (proof (B (Eqn (Add X O) X)) [induction, add1Step, (\e -> equalIfN (Add X O) X e), (\e -> equalSame (S X) e), (\e -> ifSame (Eqn (Add X O) X) (B Trueee) e), (\e -> equalIfN X O e), add1Step, (\e -> equalSame O e), (\e -> ifSame (Eqn X O) (B Trueee) e)]) B Trueee
proof以下の式に対して、
[以下のコマンド群を適用すると、
B Trueeeになって証明が成功したよ、という事です。
おわりに
という訳で、Egisonで項書き換えを用いた定理証明をおこなってみました。
ちなみに本家Egison様では、本稿の方法とは違う、型を使った定理証明機構を考えておられるみたいです。
期待が高まりますね！
ソースコード
参考文献
Egison Journal Vol.1, Vol.2
https://egison.booth.pm/ （新しいタブで開いてください）
定理証明手習い
https://www.lambdanote.com/collections/littleprover （新しいタブで開いてください）
