極小の論理プログラミングDSLmicroKanrenの使いかたと実装の紹介

microKanrenは、とてもコンパクトなScheme用の論理プログラミングDSLです。
Jason HemannとDaniel P. Friedmanによって開発されました。
論理プログラミングは、変数を含んだ制約を記述し、制約が満たせるか判定したりその制約を満たす変数を得ることを目的としています。同じ論理プログラミングDSLのkanrenシリーズ(i.g. miniKanrenやclojureのcore.logic)の最小限の機能を取り出した実装で、空行を除くと39行になります。

この記事では、microKanrenの内容、使いかたと実装の中身の紹介をします。

microKanrenとは

microKanrenは、とても小さな論理プログラミングDSLです。
コンパクトなので覚えることが少ないですが、syntax sugarがなく、内部表現むき出しで一般利用向けというより、学習用やホビー向けだと言えます。
Schemeで拡張して構文追加することもできます。

microKanrenの使いかた

microKanrenでは、制約を作ったり変数を定義したりする操作が4つあります。microKanrenではこれらの操作をgoal-constructorと呼びます。
覚えるgoal-constructorはたった4つで楽なのですが、扱うデータはところどころ内部表現がむき出しになっているため、内部表現を理解する必要があります。

また、ユーザはSchemeで新しいgoal-constructorを作ることができます。

microKanrenの4つのgoal-constructors

microKanrenは、3つの制約を作るgoal-constructorと1つの変数を新たに生成するgoal-constructorを提供しています。
制約を作るgoal-constructorは、==、conj^[1]、disjがあります。
==は、２つの値or変数が等しい制約の宣言、conjは、conjunctionの略で2つの制約のうちどちらかがなりたつかというもの、disjは、disjunctionの略で2つの制約のうちどちらも成り立つというものです。
call/freshは、1引数の手続きを受け取り、その手続きに新しい(microKanren内の)変数を作って渡します。

microKanrenの変数と状態の内部表現

直前に説明した4つのgoal-constructorは、手続きを返します。
この返ってくる手続きをgoalと呼びます。(goalを作る手続きなのでgoal-constructorと呼ばれている)
goalは状態を1つ受け取り、とりうる状態をすべて列挙しそれらを入れたリストで返します。とりうる状態が0であれば、当然空リストが返ってきます。
状態とは、各変数の値のalistと変数の定義の個数のpairです。
変数は、それぞれ整数のIDが振られており、同じIDをもつものは同じ変数として扱います。
変数の表現は、そのIDを要素数1のvectorにいれたものです。

状態の例は、こういうものです

((#(0) . 200) (#(1) . 100)) . 2)

まず、状態のcdr部が2なので、変数が2個定義されているということになります。
変数は、#(0)と#(1)の2つで、各値が100と200になっています。

あと、何も定義されていない初期状態は、(() . 0)と表現されます。変数がなにも定義されていないので、空のalistと変数の数0を組にしたものになっています。

ユーザーが独自にgoal-constructorを作る場合、状態が無限に出現するようなものが欲しいときがあります。これは、thunkを使った無限リストで表現します。これは、thunkで表現され、apply(force)すると(状態 . thunk(無限リスト) )のような結果が返ってきます。

microKanrenの使用例

microKanrenの例をいくつか示します。

call/freshと==の例

これは、変数をひとつ定義し、それが1と等しいという宣言を行う例です。
(call/fresh (lambda (x) (== x 1)))がgoalを返すので、そのgoalに初期状態(() . 0)を渡しています。定義された変数は#(0)で、それが1と等しいとしたので、(((#(0) . 1)) . 1)という状態が返ってきました。

  ((call/fresh (lambda (x) (== x 1)))
   '(() . 0))
   
  ;; => ((((#(0) . 1)) . 1))

とりうる状態がないときの例

とりうる状態が存在しない場合、microKanrenでは空リストが返ってきます。
ここでは、1と2が等しいという宣言をしています。

  ((== 1 2) '(() . 0))
  
  ;;=> ()

conjの例

conjは、2つの制約がどちらも成り立つという制約を作ります。
ここでは、xが1と等しいという宣言とxが2と等しいが両方なりたつという宣言をしています。
この2つの制約は同時に満たさないので()が返ってきます。

  ((call/fresh (lambda (x)
                 (conj (== x 1) (== x 2))))
   '(() . 0))

  ;;=> ()

disjの例

disjは、2つの制約のどちらかが成り立つという制約を作ります。
ここでは、xが1と等しいという制約とxが2が等しいという制約のどちらかが成立する制約を作っています。とりうる状態は2通りあるので、結果には2つの状態が含まれています。
その2つの状態とは、xが1と等しいという状態とxが2と等しいという状態です。

  ((call/fresh (λ (x)
                 (conj (== x 1) (== x 2))))
   '(() . 0))

  ;;=> ((((#(0) . 1)) . 1)
  ;;    (((#(0) . 2)) . 1))

microKanrenの実行

microKanrenの実装は、jasonhemann/microKanrenにあります。
この中のmicroKanren.scmを(load "./microKanren.scm")等で読みこんで使います。

実行するScheme処理系によっては、microKanrenの実装に使われているasspという手続きがないことでエラーが生じることがあります。この手続きはR6RSに含まれる機能ですが、R7RSにはないためです。
asspは、述語と連想リストを受け取り、
連想list内のkeyに述語が成り立つような最初のセルを返すというものです。
このような実装を手書きしておけば、動くはずです。

(define assp
 (lambda (pred alist)
    (find (lambda (x) (pred (car x)))
           alist)))

microKanrenの実装の解説

4つのgoal-constructorとそれに必要な補助手続きの実装の解説をします。
以下のコードは、https://github.com/jasonhemann/microKanrenから引用しています。
以下の引用しているソースコードの著作権はCopyright (C) 2013 Jason Hemann and Daniel P. Friedmanにあります。

==の実装と補助手続きwalk、unify

==は、主にwalkとunifyという補助手続きを使って実装されています。
walkとは、ある変数がどの値を取るのか再帰的に探索する手続きです。
例えば、(conj (== y 100) (== x y))という制約がある場合、walk(x)は内部でwalk(y)を呼び出し、100を返します。まだ、値が決定できない場合は、同じ値を持ちうる変数か同じ変数が返ってきます。

これは、walkの実装です。uが変数か値で、sが変数-値の連想リスト(状態のcar部)です。変数に対応する値があれば、(変数 . 変数or値)なpairを返し、変数が別の変数と対応していれば、その別の変数でwalkを再帰的に呼び出します。
walkへの入力が対応する値のない変数か値であればそれをそのまま返します。 var=?は、同じidを持つ変数かの比較手続きです。

(define (walk u s)
  (let ((pr (and (var? u) (assp (lambda (v) (var=? u v)) s))))
    (if pr (walk (cdr pr) s) u)))

unifyは、==のコアとなる補助手続きです。
2つの値が等しいという宣言が矛盾せず、どちらかの値が変数であれば、それらが等しいという情報を状態のcar部の連想リストに追加します。矛盾が生じた場合は空リストを返します。

これはunifyの実装です。u,vが値か変数で、sが変数-値の連想リストです。まず、uとvをwalkで状態に入っていないvar①か状態に入っているvar②、もともと値であった③か調べます。
①の未登録のvarであれば、walkの結果はvarになり、他方の値を連想リストsに登録します。ext-sは、変数、値、連想リストを引数にとり、変数、値が等しいという関係を連想リストsに登録します。
②の状態に入っているvarであれば、walkの結果は(変数 . 変数or値)pairが返って来ます。
walkした結果が両方とも(変数 . 変数or値)なpairであればcar部の変数同士を等しいという関係を連想リストsに登録し、cdr部の変数or値　同士が異なる値でなければ連想リストsに登録し、異なる値であれば#fを返します。

③の値同士であれば、eqv?で等しいかチェックします。等しければ連想リストsをそのまま返し、そうでなければ#fを返します。

(define (unify u v s)
  (let ((u (walk u s)) (v (walk v s)))
    (cond
      ((and (var? u) (var? v) (var=? u v)) s)
      ((var? u) (ext-s u v s))
      ((var? v) (ext-s v u s))
      ((and (pair? u) (pair? v))
       (let ((s (unify (car u) (car v) s)))
         (and s (unify (cdr u) (cdr v) s))))
      (else (and (eqv? u v) s)))))

これが==の実装です。uとvが変数or値で、s/cが状態です。(lambda (s/c) ...)がgoalです。unifyした結果が成功(つまり、連想リストが返ってくる)であれば、その連想リストから新しい状態を作りそれが1つ含むだけのリストを返します。==の引数は、変数or値でcall/freshが作るgoalは受け取れないため、==内で変数は増えません。したがって、変数の数は(cdr s/c)から変わりません。unifyした結果が#fで失敗であれば、()を返します。

(define (== u v)
  (lambda (s/c)
    (let ((s (unify u v (car s/c))))
      (if s (unit `(,s . ,(cdr s/c))) mzero))))

disjとその補助手続きのmplus

mplusの実装は以下のとおりです。disjのコアとなる手続きです。mplusは状態のリストの2つをとります。基本的には、結果のリストを結合したものを返します。実装の(procedure? $1)部分を除けば実質appendです。

結果のリストには、遅延リストを含みます。これは状態数が無限あるいは大きすぎるときの結果リストのために使います。遅延リストの表現は、cdr部がthunk (delayした結果のような)になっています。
force(1回apply)すると、(状態 . 遅延リスト)なペアになります。(procedure? $1)は遅延リストのための処理で、mplusは実質、lazy-appendとなっています。

(define (mplus $1 $2)
  (cond
    ((null? $1) $2)
    ((procedure? $1) (lambda () (mplus $2 ($1))))
    (else (cons (car $1) (mplus (cdr $1) $2)))))

disjは、goalを2つ受け取り、goalに状態をそれぞれ適用して得られた結果のリストをmplusに渡すだけです。

(define (disj g1 g2) (lambda (s/c) (mplus (g1 s/c) (g2 s/c))))

conjとその補助手続きのbind

bindの実装は以下のとおりです。bindは、状態のリストとgoalをとります。
状態のリスト内のすべての各状態をgoalに適用し、それぞれでた状態すべてを1つのリストにまとめます。
実質、(append-map goal state-list)のような処理です。

bindも遅延リストをサポートしています。遅延リストを入れると、のこり全てにgoalを遅延的に適用するような遅延リストを返します。

(define (bind $ g)
  (cond
    ((null? $) mzero)
    ((procedure? $) (lambda () (bind ($) g)))
    (else (mplus (g (car $)) (bind (cdr $) g)))))

conjは、goalを2つ受け取り、1つのgoalに状態を適用した結果ともう1つのgoalをbindに渡します。

(define (conj g1 g2) (lambda (s/c) (bind (g1 s/c) g2)))

call/fresh

call/freshは、値を一つとる本体がgoalな手続きfを受け取り、goal(lambda (s/c) ...)を返します。
goal内で、新しいvarを作りと変数の数(状態のcdr部)を+1した新しい状態を作ります。
そして、手続きfに新しいvarを渡して得られたgoalに新しい状態を渡します。

(define (call/fresh f)
  (lambda (s/c)
    (let ((c (cdr s/c)))
      ((f (var c)) `(,(car s/c) . ,(+ c 1))))))

最後に

microKanrenの使いかたと実装について説明しました。

microKanrenは機能が少ないため、ユーザがSchemeで拡張用のgoal-constructorを作る必要があります。miniKanrenの機能を追加するという例が、miniKanren-wrappers.scmにあります。それも合わせてみると良いでしょう。

脚注

1. Clojureのconjは、conjoinなので関係はないです