Prologの処理系をTypeScriptで書いてみた

言語仕様の一部しか実装していませんが、一応動くものができたので公開してみます。(v10以降の)Node.jsが必要です。

github.com

Prologとは

論理型プログラミング言語の一つです。論理学をプログラミング言語に落とし込んだようなもので、「ある論理式の集合からある論理式が導けるか」みたいなものが判定できます。もう少し広げて、(論理式内に自由変数を導入し)「論理式の集合が与えらたとき、その中の各自由変数をどのような項で代入するとゴールとなる論理式が導けるか」というクエリの処理が可能です。

Wikipediaの記事が恐ろしいほど詳しいです。よく使われる処理系としてSWI-Prologがあります。

使い方

npmパッケージとして公開しています。以下のようにして使えます。

$ npm install ts-prolog -g
$ ts-prolog

使用例

以下のようなファイルをrules.plとして保存します。足し算の定義や掛け算の定義、自然数の定義などが書いてあります。

mult(z, X, z).
add(z, Y, Y).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
mult(s(X), Y, Z) :- mult(X, Y, P), add(P, Y, Z).
nat(z).
nat(s(X)) :- nat(X).

以下のような形で使用できます。足し算してみたり、掛け算してみたり、自然数の集合を取得してみたり、足し算と掛け算の2つ式を連立方程式としてその解を求めたり、ということをしています。

$ ts-prolog
> ['rules.pl'].
fact added: mult(z, X, z)
fact added: add(z, Y, Y)
rule added: add(s(X), Y, s(Z)) :- [add(X, Y, Z)]
rule added: mult(s(X), Y, Z) :- [mult(X, Y, P), add(P, Y, Z)]
fact added: nat(z)
rule added: nat(s(X)) :- [nat(X)]

> add(s(z), s(s(z)), X).
[X -> s(s(s(z)))]  (ENTER)
search finished

> add(s(z), X, s(s(s(z)))).
[X -> s(s(z))] (ENTER)
search finished

> mult(s(s(z)), s(s(s(z))), X).
[X -> s(s(s(s(s(s(z))))))] (ENTER)
search finished

> nat(X).
[X -> z] (ENTER)
[X -> s(z)] (ENTER)
[X -> s(s(z))] (ENTER)
[X -> s(s(s(z)))] (ENTER)
[X -> s(s(s(s(z))))] (Ctrl-C)

> add(X, Y, s(s(z))).
[X -> z, Y -> s(s(z))] (ENTER)
[X -> s(z), Y -> s(z)] (ENTER)
[X -> s(s(z)), Y -> z] (ENTER)
search finished

> add(X, Y, s(s(z))), mult(X, Y, s(z)).
[X -> s(z), Y -> s(z)] (ENTER)
search finished

実装について

パーサ

特にライブラリは使わずに、自分で簡単なものを実装してみました。LR構文解析器などを作っても良かったのですが、比較的文法が単純なことから、正規表現などをつかってゴリゴリやってしまっています。完璧ではないはずです。

本体

  • ファンクタ(「使用例」のadd, natなど)を表すFunctorクラス
  • 定数(「使用例」のzなど)を表すConstantクラス
  • 変数(「使用例」のX, Yなど)を表すVariableクラス
  • ファンクタの項への適用(add(X, Y, Z)など)を表すApplicationクラス

を定義し、項を表すTerm型をtype Term = Functor | Constant | Variable | Applicationのようにして定義しています。

また、次のようなクラスも用意しています。

  • 述語を表すPredicateクラス
  • ファクト(例: nat(z).でゼロは自然数であることを表現する)を表すFactクラス
  • ルール(例: nat(s(X)) :- nat(X).でXが自然数ならばXに1を足したものが自然数であることを表現する)を表すRuleクラス
  • ゴール(例: nat(X).で自然数であるようなものを探したいことを表現する)を表すGoalクラス

ゴールとファクト/述語を単一化(unification)するために制約を表すConstraintクラスを用意しており、Constraint.unify(terms: Term[])によって、単一化ができるようになっています(自由変数への項の代入を表すSubstitutionクラスを返します)。

一番メインとなるのがSpaceクラスで、これはルールの集合とファクトの集合です。Space.query(goals: Goal[])によって、その空間内での探索が始まります。これは基本的には「自由変数から項へのマッピング」の列を返します。例えば上の例だとnat(X)[[X -> z], [X -> s(z)], ...]のようなものを返します。これは無限列になることがしばしばあるため、イテレータを返すようにしています。

SWI-PrologなどはDFSですが今回はキューを用いてBFSでやってみています。無限ループに陥るゴールの集合が少し変わります。自分はこちらのほうが直感的な気がします。

CLI

インターフェイスについては特にユーザーランドのライブラリなどは用いず、Node.jsコアのreadlineモジュールを利用しました。Ctrl-Cのキャプチャなど、案外いろいろなことができます。

ユーザーからのインプットを受け取り、次のようなことをします。

  • ファイルの読み込みが要求されたらそのファイルを開いてルールとゴールを追加する
  • クエリ(ゴールの集合)が入力されたらそれに対する答え(自由変数から項へのマッピング)を一つずつ(すべての探索が終了するかCtrl-Cが押されるまで)出力する

ソースコード

こちらで公開しています。なにか質問や疑問、バグなどあれば教えていただけると嬉しいです。

github.com