完成したものは僕のGitHub Pagesで公開しています。 連言やカットなどの機能は省略したのでほぼ導出原理(の証明の探索)そのままになっています。
Prologの文法
Prologのプログラムはホーン節と呼ばれる述語論理の論理式の列から成ります。さらにホーン節は仮定を表すプログラム節と質問を表すゴール節の二種類に分けられます。 プログラム節の文法は
A :- B_1, ... , B_n.
または
A.
のような形をしており、それぞれ「B_1からB_nがすべて成り立つならばAが成り立つ」と「Aは無条件で成り立つ」という仮定を表します。 ゴール節の文法は
C_1, ..., C_n.
の形であり、「C_1, ... ,C_nは充足可能か？もしそうならそのような代入を求めよ」という質問を表します。
例えばプログラム節が
p(X) :- q(X), r(X). q(a). r(a). p(b).
でありゴール節が
p(X).
であったならば答えはX=aとX=bという代入になります。
処理系のアルゴリズム
Prologの処理系は事前にプログラム節を読み取り、ゴール節で与えられるクエリを投げられたときに、そのゴール節を充足させるような代入を探索します。これは導出原理の証明図を探すことに対応します。述語論理の充足可能問題の決定不能性からこの探索は停止する保証がありません。
ゴール節が空なら充足可能でその時点での代入を返す
ゴール節が空でないならその中から論理式(Cとする)を一つとる
- プログラム節の結論の中でCとマッチするものがあるならCをその節の仮定に置き換える
先ほどの例で言うと、 ゴール節のp(X)はプログラム節p(b).とp(X) :- q(X), r(X).の結論にマッチします。 前者の場合は仮定が存在しないのでゴール節が空になり探索が終了し、X=bという答えが出ます。 後者の場合は仮定があるのでゴール節がq(X)とr(X)に置き換わり探索が続きます。 q(X),r(X)はそれぞれq(a),r(a)とマッチするので探索は終了します。
このマッチするかを判定するアルゴリズムは単一化と呼ばれMLの型推論などにも用いられています。
実装
字句解析・構文解析にはpegを使いました。nomの方が慣れていたのですが、「大文字の列」などを認識するのが面倒だったのでpegを採用しました。 ソースコードのRust側はこちらにWasmを利用するJavaScript側はこちらに公開しています。
