はじめに
μKanren はリレーショナル（論理）プログラミング言語の miniKanren のエッセンスを 40 行未満の scheme にまとめたものです。μKanren をマイクロカーネルとして、その上に miniKanren を実装し直すこともできます。
...というものらしいのですが、実を言うとあまりよく理解できていません。
μKanren を学ぶのに一番よい方法は scheme 以外の言語に μKanren を移植することであるため、いろいろな言語に μKanren が移植されている、ということなのでマイ・GHC でも μKanren を動かしてみることにします。
Prolog 版 μKanren を横目に見つつ、論文 の最後にある scheme のコードを移植してみます。
実装
変数と状態
μKanren では変数と変数にバインドされた値のペアからなる連想リスト（ストリーム）を操作することで推論を実行していきます。
この連想リストを、μKanren の変数と、その変数に現在バインドされている値のペア var(C)=X （ここで C は変数のインデックス番号、X はバインドされた値）からなるリストで表現することにします。
例えば、変数 var(1) に値 5 が バインドされている状況は、[var(1)=5] という単一要素のリストで表せます。
さらに、この連想リストと現在いくつのμKanren 変数が存在するかを表すカウンタのペアをした項 state/2 を「状態」と呼ぶことにします。
初期状態は、空の連想リストとカウンタ値０からなる状態です。初期状態を返す述語は以下のように書けます（Prolog 版そのまま）。
% empty_state(-S0)
empty_state(S0) :-
S0 = state([], 0).
今の状態から、μKanren 変数を新たに一つ割り当てる述語を以下のように書くことにします（これも Prolog 版そのまま）。
% var(-Var, +State, -State2)
var(Var, state(Sub, C0), State2) :-
true |
C := C0 + 1,
Var = var(C),
State2 = state(Sub, C).
割当前の状態（第２引数）元に、割り当てた変数（第１引数）および割当後の状態（第３引数）を返します。
walk オペレータ
特定のμKanren 変数を連想リスト上で検索し、当該変数にバインドされた値を返すのが walk です。
walk(var(C), Sub, V) :-
seek(var(C), Sub, V0),
continue_walk_if_seek_success(var(C), V0, Sub, V).
otherwise.
walk(U, _, V) :-
true |
V = U.
seek(_, [], V0) :- true | V0 = fail.
seek(Var, [Var=V1|_], V0) :- true | V0 = success(V1).
otherwise.
seek(Var, [_|Sub], V0) :- seek(Var, Sub, V0).
continue_walk_if_seek_success(U, success(V0), Sub, V) :- walk(V0, Sub, V).
continue_walk_if_seek_success(U, fail, _, V) :- true | U = V.
ストリームに μKanren 変数が定義済みか調べ（seek/3）、定義が見つかったかどうかで更に walk を再帰的に実行するか、そのまま値として返すか（continue_walk_if_seek_success）します。
seek/3 は検索に成功した場合には success でラップされた値を、失敗した場合には fail を返します。
continue_walk_if_seek_success はその結果が success ならさらに再帰的に walk/3 を呼び出し、fail ならばそこで再起呼び出しを停止します。
unify
unify/4 は、与えられた状態（第３引数）の元で２つのμKanren 変数あるいは値（第１引数および第２引数）について単一化を試みます。
単一化に成功すれば、単一化された状況を含む状態を、単一化に失敗すれば空を返します（第４引数）。
% unify(+U0, +V0, +St0, -Str)
unify(U0, V0, St0, Str) :-
true |
Str = thunk(Str1, delayed_unify(U0, V0, St0, Str1)).
delayed_unify(U0, V0, state(Sub0,C), Str) :-
walk(U0, Sub0, U1),
walk(V0, Sub0, V1),
unification(U1, V1, Sub0, Sub),
put_result_state_if_success(Sub, state(Sub, C), Str).
put_result_state_if_success([], _, Str) :-
true |
Str = [].
put_result_state_if_success([_|_], State, Str) :-
true |
Str = [State].
unification(U, U, Sub0, Sub2) :-
true |
Sub2 = Sub0.
unification(VarU=ValU, VarV=ValU, Sub0, Sub2) :-
unify(VarU, VarV, Sub0, Sub1),
unify(ValU, ValV, Sub1, Sub2).
unification(var(C), var(C), Sub0, Sub2) :-
true |
Sub2 = Sub0.
otherwise.
unification(U, V, Sub0, Sub2) :-
unification2(U, V, Sub0, Sub2).
unification2(var(C), V, Sub0, Sub2) :-
true |
Sub2 = [var(C)=V|Sub0].
unification2(U, var(C), Sub0, Sub2) :-
true |
Sub2 = [var(C)=U|Sub0].
otherwise.
unification2(_, _, _, Sub2) :-
true |
Sub2 = [].
サンク
ここで、unify/4 での遅延評価を実現するためにサンクを返すことにしました。
具体的には、値 X を実現させる述語 P からなる項 thunk(X, P) を返して、これを受け取った側は具体的な値が必要になったら call(P) で P を実行したうえで X を見る、という取り決めにしました。
サンクから値を取得する述語を書くと、以下のようになります:
% pull(+T, -V)
pull(thunk(X, P), V) :-
call(P), pull(X, V).
otherwise.
pull(T, V) :-
V = T.
サンクから得た値がリスト、あるいは項で、その要素が更にサンクである場合には以下のように再帰的にサンクを解決する必要があります。
% take_all(+T, -V)
take_all(T, V) :-
pull(T, T1),
take_all_aux(T1, V).
take_all_aux([], V) :-
true |
V = [].
take_all_aux([T|Ts], V) :-
true |
V = [V1|V2],
pull(T, V1),
take_all(Ts, V2).
サンクが無限リストを表現している場合にはサンクの評価を適当なところで打ち切りたい、ということがほとんどでしょう。
% take(+N, +T, -V)
take(0, T, V) :-
true |
V = [].
take(N, T, V) :-
pull(T, T1),
take_aux(N, T1, V).
take_aux(_, [], V) :-
true |
V = [].
take_aux(N, [T1|Ts], V) :-
true |
pull(T1, V1),
N1 := N - 1,
take(N1, Ts, V2),
V = [V1|V2].
サンクでなく有限長バッファ通信 の技法を使う方がより GHC らしくてよかったかもかもしれません。
call_fresh, disj, conj
論文にある Schema 版 call/fresh は新しい変数を確保して与えられたゴールを実行する関数を返す関数（ゴールコンストラクタ）ですが、Prolog 版実装に倣って新しい変数を確保してゴールを呼び出す述語にしました:
% call_fresh(-X, +Goal, +St0, -Str)
call_fresh(X, Goal, St0, Str) :-
true |
var(X, St0, St),
call(Goal, St, Str).
disj, conj も論文ではゴールコンストラクタということになっていますが、サンクを返す形にしました。
述語 disj/4 は mplus/3 を遅延実行するサンクを返します:
% disj(+Goal1, +Goal2, +St0, -Str)
disj(G1, G2, St0, Str) :-
true |
Str = thunk(Str0, delayed_disj(G1, G2, St0, Str0)).
delayed_disj(G1, G2, St0, Str) :-
call(G1, St0, Str1),
call(G2, St0, Str2),
mplus(Str1, Str2, Str).
述語 conj/4 は bind/3 を遅延実行するサンクを返します:
% conj(+Goal1, +Goal2, +St0, -Str)
disj(G1, G2, St0, Str) :-
true |
Str = thunk(Str0, delayed_disj(G1, G2, St0, Str0)).
delayed_disj(G1, G2, St0, Str) :-
call(G1, St0, Str1),
call(G2, St0, Str2),
mplus(Str1, Str2, Str).
いずれも、ゴールの呼び出しに call/3 を使っているのがミソです。
これにより、call_fresh/4、disj/4、conj/4 に与えるゴールを関数のような見た目で書けます（これについては後で例を示します）。
mplus
述語 mplus は基本的には２つの連想リスト（第１引数、第２引数）をつなぎ合わせたもの（第３引数）を返すオペレータです。
与えられた連想リストがサンクの場合には、mplus を遅延実行するサンクを返します。
% mplus(+S1, +S2, -Str)
mplus([], S2, Str) :-
true | Str = S2.
mplus(thunk(X1, P1), S2, Str) :-
true |
Str = thunk(Str0, delayed_mplus(P1, X1, S2, Str0)).
mplus([S|S1], S2, Str) :-
true |
mplus(S1, S2, Sts),
Str = [S|Sts].
delayed_mplus(P1, X1, S2, Str) :-
call(P1),
mplus(S2, X1, Str).
bind
述語 bind は連想リスト（第１引数）に与えられたゴール（第２引数）を適用し、その結果となる連想リスト（第３引数）を返すオペレータです。
与えられた連想リストがサンクの場合には、bind を遅延実行するサンクを返します。
% bind(+St0, +Goal, -Str)
bind([], _, Str) :-
true |
Str = [].
bind(thunk(X, P), G, Str) :-
true |
Str = thunk(Str0, delayed_bind(P, X, G, Str0)).
bind([S|Ss], Goal, Str) :-
call(Goal, S, Str1),
bind(Ss, Goal, Str2),
mplus(Str1, Str2, Str).
delayed_bind(P, X, G, Str2) :-
call(P),
bind(X, G, Str2).
μKanren を実行してみる
実装したもの を実際に動かしてみることにします。
five_or_six
変数の値が 5 か 6 のどちらかであるという状態を作って、それを表示してみます。
test_five_or_six :-
empty_state(S0),
call_fresh(X,
( five_or_six(X), take_all ),
S0, S2),
pp(0, S2, P, [nl]),
outstream([writeln('five_or_six(X), take_all'),
writeln(' -> ') | P]).
five_or_six(X, Sub0, Sub2) :-
disj(unify(X, 5),
unify(X, 6), Sub0, Sub2).
ここで、pp/4 は実行結果を pretty-print するために作った述語です。
以下のような実行結果が得られます:
five_or_six(X), take_all
->
[
state([var(1)=5],1),
state([var(1)=6],1)
]
var(1) が 5 にバインドされた状態と、var(1) が 6 にバインドされた状態の２つを応答しています。
ここで、call_fresh に five_or_six(X), take_all というゴールを与えていますが、これが実際に呼び出される際には入出力ストリーム引数が追加されて
five_of_six(X, St0, St1),
take_all( St1, St2)
のように呼び出されます。このような引数の付与を自動的に行ってくれるのが call/3 の便利なところです。
fives, sixes
変数の値が 5 である状態のストリーム、変数の値が 6 である状態のストリームをそれぞれ作って表示してみます。
結果はサンクによる無限ストリームなので、無限ストリームの先頭 10 個の値を表示することにしました。
test_fives :-
empty_state(S0),
call_fresh(X,
( fives(X), take(10) ),
S0, S2),
pp(0, S2, P, [nl]),
outstream([writeln('fives(X), take(10)'),
writeln(' -> ') | P]).
fives(X, Sub0, Sub2) :-
disj(unify(X, 5), fives(X), Sub0, Sub2).
test_sixes :-
empty_state(S0),
call_fresh(X,
( sixes(X), take(10) ),
S0, S2),
pp(0, S2, P, [nl]),
outstream([writeln('sixes(X), take(10)'),
writeln(' -> ') | P]).
sixes(X, Sub0, Sub2) :-
disj(unify(X, 6), sixes(X), Sub0, Sub2).
実行結果は
fives(X), take(10)
->
[
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1),
state([var(1)=5],1)
]
sixes(X), take(10)
->
[
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1)
]
で、それぞれ var(1) が 5 に束縛された状態のストリーム、var(1) が 6 に束縛された状態のストリームという形で得られています。
fives_and_sixes
論文にある、var(1) が 5 に束縛された状態と 6 に束縛された状態を交互に返す例です。
test_fives_and_sixes :-
empty_state(S0),
call_fresh(X,
( fives_and_sixes(X), take(10) ),
S0, S2),
pp(0, S2, P, [nl]),
outstream([writeln('fives_and_sixes(X), take(10)'),
writeln(' -> ') | P]).
fives_and_sixes(X, Sub0, Sub2) :-
disj(fives(X), sixes(X), Sub0, Sub2).
実行結果:
fives_and_sixes(X), take(10)
->
[
state([var(1)=5],1),
state([var(1)=6],1),
state([var(1)=5],1),
state([var(1)=6],1),
state([var(1)=5],1),
state([var(1)=6],1),
state([var(1)=5],1),
state([var(1)=6],1),
state([var(1)=5],1),
state([var(1)=6],1)
]
conj
conj の動作を確認してみます。
fives_and_sixes とsixes を conj して 6 だけのストリームを作ってみます。
test_fives_and_sixes2 :-
empty_state(S0),
call_fresh(X,
( conj(fives_and_sixes(X), sixes(X)), take(10) ),
S0, S2),
pp(0, S2, P, [nl]),
outstream([writeln('conj(fives_and_sixes(X), sixes(X)), take(10)'),
writeln(' -> ') | P]).
実行結果:
conj(fives_and_sixes(X), sixes(X)), take(10)
->
[
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1),
state([var(1)=6],1)
]
２つの変数
call_fresh を重ねることで、２つの変数を取り扱えるはずです。
test_fives_and_sixes3 :-
empty_state(S0),
call_fresh(X, (fives_and_sixes(X),
test_fives_and_sixes3_Y,
take(4) ), S0, S2),
pp(0, S2, P, [nl]),
outstream([write('(fives_and_sixes(X), take(4)), '),
writeln('(fives_and_sixes(Y), take(4))'),
writeln(' -> ') | P]).
test_fives_and_sixes3_Y(thunk(St0, P), St1) :-
call(P), test_fives_and_sixes3_Y(St0, St1).
test_fives_and_sixes3_Y([], St1) :-
true |
St1 = [].
test_fives_and_sixes3_Y([S|Ss], St1) :-
true |
call_fresh(Y, ( fives_and_sixes(Y), take(4) ), S, S1),
St1 = [S1| thunk(S0, test_fives_and_sixes3_Y(Ss, S0))].
一応、それっぽい結果が得られました。
(fives_and_sixes(X), take(4)), (fives_and_sixes(Y), take(4))
->
[
[
state([var(2)=5,var(1)=5],2),
state([var(2)=6,var(1)=5],2),
state([var(2)=5,var(1)=5],2),
state([var(2)=6,var(1)=5],2)
],
[
state([var(2)=5,var(1)=6],2),
state([var(2)=6,var(1)=6],2),
state([var(2)=5,var(1)=6],2),
state([var(2)=6,var(1)=6],2)
],
[
state([var(2)=5,var(1)=5],2),
state([var(2)=6,var(1)=5],2),
state([var(2)=5,var(1)=5],2),
state([var(2)=6,var(1)=5],2)
],
[
state([var(2)=5,var(1)=6],2),
state([var(2)=6,var(1)=6],2),
state([var(2)=5,var(1)=6],2),
state([var(2)=6,var(1)=6],2)
]
]
しかし、やや煩雑なプログラムになってしまいました。
GHC は単一代入なので、複数回呼び出されるλ的なものを記述するにはλ相当の部分を別述語に切り出して書く必要があるのでこのようになっています。
多分、このあたりは Prolog 版も同じことになるはずですが、GitHub には多変数を取り扱う例がないのでどうやっているのかはよくわかりません。
まとめ
GHC 上で μKanren を動かしてみました。
なんとか動くようにするのが精一杯で、μKanren 自体についての理解が深まった感じはあまりないというのが正直なところです。