1

我开始研究一些 minikanren，并编写了这个例子来计算列表中的 1 位。

(define (count xs n)
  (conde
   [(== xs '()) (== n 0)]
   [(fresh (a b)
           (== xs (cons a b))
           (conde
            [(== a 0) (count b n)]
            [(== a 1) (count b (- n 1))]))]))

现在以下工作正常

> (run* (q) (fresh (a b c) (== q (list a b c)) (count q 1)))
'((0 0 1) (1 0 0) (0 1 0))

但是如果我改变目标的顺序，程序不会终止

> (run* (q) (fresh (a b c) (count q 1) (== q (list a b c))))
. . user break

这已经是我不完全理解的东西了，目标的顺序重要吗？在哪些方面？我想我明白，即使是随后的目标也会造成足够的限制，从而终止搜索，但我当然一定错过了一些东西。

探索更多这个问题，我看到了

> (run 3 (q) (fresh (a b c) (count q 1) (== q (list a b c))))
'((0 0 1) (0 1 0) (1 0 0))
> (run 4 (q) (fresh (a b c) (count q 1) (== q (list a b c))))
. . user break

所以我知道它试图寻找比现有更多的答案。我现在的怀疑是当子目标

(== xs (cons a b))

拆分列表没有足够的约束b来使搜索有限，这听起来很合理，因为除了外部之外没有任何东西谈论列表的尾部(== q (list a b c))。期望不终止似乎更合理，因为没有说明cin 的内容(== q (list a b c))，它可能是另一个列表（是真的吗？），但是程序的交换版本如何终止？

因此我尝试了

(define (bit x)
  (conde [(== x 0)] [(== x 1)]))

和

> (run 4 (q) (fresh (a b c) (bit a) (bit b) (bit c) (count q 1) (== q (list a b c))))
. . user break

但它仍然没有终止，所以也许问题不是我想的那样。

总的来说，我的理解中一定有一些我遗漏的东西，任何人都可以澄清这一切并指出做这件事的正确方法是什么？

4

0 回答 0