microKanrenで始めるlogic programming入門 (1)

scheme logic programming

microKanrenとは

microKanrenの話の前にまずminiKanrenの紹介を。

miniKanrenは埋め込み言語としての利用を想定した論理プログラミング言語で、実際に各種言語上での実装が存在する。The Reasoned SchemerはminiKanrenをscheme上での実例を示しながら紹介するという内容だし、clojureではcore.logicで miniKanrenとほぼ同様のDSLが提供されている。miniKanrenが内部でやっていることはほぼprologのそれと同じで、つまり探索による単一化だ。(もっともminiKanrenもprologのこともよくわかっていないのでこの言い方が正確かは微妙だけれど…)

DSLという性格もあってminiKanrenはコンパクトにまとまった言語で、例えばschemeの実装では784行におさまっている。microKanrenはこのminiKanrenの論理プログラミングのエッセンスを抽出した言語で、そのコア部分のschemeの実装はわずか39行(!)に収まっている。スゴイシンプル。この記事ではmicroKanrenの実装を通じていわゆる論理プログラミング言語が内部で何をやっているかということを紹介していきたい。

一次資料は以下のものがある。ぶっちゃけこっちを読んだ方が早い。

varとgoalとstate

microKanrenはものすごくシンプルでユーザーフレンドリーな部分なんて全くないから基本的な概念を理解しておかないと実例が何やってるかをそもそも理解できない。

varは変数を表す。この変数はschemeのそれではなく、microKanrenのものだ。ユニークなオブジェクトだという理解で問題ない。ちなみに単一化というのはgoalに基いてこのvarと実際の値を対応付ける操作のことを言う。多分。

(var 3)
; => #(3)
(let ((v (var 2))
      (w (var 3)))
    (var=? v w))
; => #f

goalは変数をどのように単一化するかを示すもので、「宣言」と言った方がわかりやすいかもしれない。microKanrenではgoalを生成するオペレータが4つ存在する。==, call/fresh, disj, conjだ。

(== x y)
; 「xとyは同一のものである」という宣言
(call/fresh (lambda (x) ...))
; xに変数を束縛した上で宣言する
(disj g1 g2)
; 「g1かg2のどちらかの宣言が成り立つ」という宣言
(conj g1 g2)
; 「g1とg2のどちらの宣言も成り立つ」という宣言

stateは変数の単一化の状態を表す。car部には現時点での変数と値の対応がalistで入っていてcdr部には現時点で生成された変数の個数が入っている。stateに問い合わせることでどの変数がどういう値を持つかを調べることができる。

; stateとしてありうるのはこんなのとか
(((#(0) . 2)) . 1)
; こんなのとか
(((#(1) . 2) (#(0) . #(1))) . 2)

goalが具体的にどういうものかというと、stateを受け取ってstateのリストを返す関数だ。つまり、goalは現在の単一化の状態を受け取って、それと宣言の内容からありうる全てのstateを返す。

ちょっと実例

というわけで簡単な例はこんな感じになる。

;; 初期状態では何の対応付けもされてないし変数も生成されていない
(define empty-state '(() . 0))

(define (five x) (== x 5))
(define (six x) (== x 6))

((call/fresh (lambda (x) (five x))) empty-state)
; => ((((#(0) . 5)) . 1))

((call/fresh (lambda (x) (disj (five x) (six x)))) empty-state)
; => ((((#(0) . 5)) . 1) (((#(0) . 6)) . 1))

((call/fresh (lambda (x) (conj (five x) (six x)))) empty-state)
; => ()

microKanrenの内部についてはまた今度。最も39行しかないんだし元コード読んだ方が早い。