recursive miniKanren

scheme

cKanrenもminiKanrenも再帰関係を記述できない

> (run* (q) (== q `(3 ,q))) ;; should be #0 = ( 3 . #0#)
'()

実行すると「そんな関係は存在しない」という答 '() が帰ってくる。説明のためもう少し複雑な例を使う。これでも同様

> (run* (q) 
    (fresh (x)
       ( == x `(3 ,x))
       ( == q `(1 5 ,x  7))
       ))
'()

この本来の答は無限に展開されるList

(1 5  #0=(3  #0#) 7 )
=
(1 5 (3  (3  (3  (3 ... ))))  7)

になるはず。
これを扱えるように拡張した

https://github.com/niitsuma/Racket-miniKanren/blob/recursive/mk.rkt
が本体。同じディレクトリの他のファイルがなくても、このファイルと
https://github.com/niitsuma/Racket-miniKanren/blob/recursive/racket-compat.rkt
の２つがあれば動く

https://github.com/niitsuma/Racket-miniKanren/tree/recursive
のディレクトリには他の拡張ユーティリティがついでにおかれているが、とりあえず使うだけなら関係ない


再帰で無限展開されるのを避けるなら無限リストを単純に変数に置き換えて

> (run* (q) 
    (fresh (x)
       ( == x `(3 ,x))
       ( == q `(1 5 ,x  7))
       ))
(1 5  _.0 7)

が答でもよいが、これでは再帰関係の情報が失われてしまうので

( (1 5 ( ==> _.0  (3 _.0) )  7)  )

という答を返すようにした。

( (1 5  #0=(3  #0#)  )

だと #0=_.0 を表現できない(それともこっちの表記法の方がいいの？)

ここで ==>　を再帰関係を表現するタグとして扱っている。

( ==> _.0   (3 _.0) )

の意味は
_.0 　が (3 _.0)　に展開される（単純に展開したら無限に展開される）という意味



再帰を含まない部分、例えば以下の例の1 5 7は普通のminiKanrenと同じように答を返す。再帰のある部分だけが ==> から始まるListで置き換えられる

> (run* (q) 
    (fresh (x)
     ( == x `(3 ,x))
     ( == q `(1 5 ,x  7))

( (1 5 ( ==> _.0  (3 _.0) )  7)  )


他の実行例はテストコード
https://github.com/niitsuma/Racket-miniKanren/blob/recursive/test.scm
の

(define mk-cyclic-walk-tests
  (schemeunit:test-suite
 ...

以下にいくつか書いた

フーリエ級数展開

同じパターンを繰り返す無限Listを表現できるので、フーリエ級数展開のような事もできるので実行例に加えた。
任意の繰り返しパターンの検出ができる。詳しくはReadmeに追記した



処理系

racketで動くようにしてあるが　dict-ref dict-has-key? の関数を他の処理系用に作れば動くと思う

型推論

miniKanrenで型推論をするこの例を
https://github.iu.edu/webyrd/Quines/blob/master/code/infer.scm
recursive miniKanren　で動かすと、同じ出力とさらにプラスでこんな結果も出力してくれる

(run 10 (q) (fresh (t exp) (!- exp '() t)  (== `(,exp => ,t) q)))

> '( ....

(((lambda (_.0) (_.0 _.0)) => (-> (-> (==> _.1 (-> _.1 _.2)) _.2) _.2))
   : (sym _.0))
...

  (((lambda (_.0) (lambda (_.1) (_.1 _.1)))
    =>
    (-> _.2 (-> (-> (==> _.3 (-> _.3 _.4)) _.4) _.4)))
   : (=/= ((_.0 . lambda))) (sym _.0 _.1))
...
)

ここで

(　(lambda (_.0) (_.0 _.0))　 => (-> (-> (==> _.1 (-> _.1 _.2)) _.2) _.2))

の意味は

(lambda (_.0) (_.0 _.0))

で _.0　の型が関数

(-> (-> (-> (-> ...) _.2) _.2) _.2)

な事を意味している。(_.0 _.0)　で

(-> (-> (-> (-> ...) _.2) _.2) _.2)

の関数をそれ自身に適用すると結果は _.2　となり間違ってはいない。無限Listの型推論もできる事がわかる。

関連

 (run* (q)  
　　(membero 3 q) )

の無限ループを回避する別な方法を提案。

  • HaskellのminiKanrenでは同様の無限List処理を行っている記述がある https://github.com/jvranish/MiniKanrenT のReadmeによると My implementation will not go into an infinite loop if a unification is circular. There is no "occurs check" and it doesn't need one.

関連日本語リンク