查询变量在特定位置时不终止

Question

考虑 this blog post 作者使用 reverso:

实现回文关系

(defn reverso [l r]
  (conde
    [(== l ()) (== r ())]
    [(fresh [la ld ldr]
      (conso la ld l)
      (appendo ldr (list la) r)
      (reverso ld ldr))]))

当我运行(run* [q] (reverso q [1 2 3]))时，输出为([3 2 1])。但是，当我运行(run* [q] (reverso [1 2 3] q))时，程序并没有终止。我能够通过 run 1.

明确请求一个结果来获得正确的结果

在试验时，我能够使用 defne:

自己实现相同的功能

(defne conjo2 [l a la]
       ([[] _ [a]])
       ([[c . bs] _ [c . cs]] (conjo2 bs a cs)))

(defne reverso [l r]
       ([[] []])
       ([[a . ls] _]
        (fresh [rs]
               (conjo2 rs a r)
               (reverso ls rs))))

但存在同样的问题。但是，如果我将自定义 conjo2 更改为 core.logic/conjo，则变量在非终止期间的位置会发生变化。

为什么程序不终止具有查询变量特定位置的一般查询？
为什么指定 run 1 成功，但一旦 run 2 程序就不会终止？

Answer 1

问题是，当你给 appendo 一个新的左边变量和一个新的结果变量时，它可以产生任意多个答案，其中 none 个将导致一个解决方案对于您的总体 reverso 问题。见证 the definition of appendo:

(defne appendo
  "A relation where x, y, and z are proper collections,
  such that z is x appended to y"
  [x y z]
  ([() _ y])
  ([[a . d] _ [a . r]] (appendo d y r)))

如果x参数为空则终止（结果是y）；否则，它假定 x 和结果 z 都是非空列表并递归调用自身。如果可以证明 x 或 z 具有有限长度，或者如果它们共享的索引在两个列表中具有不同的值，则这将终止。您永远不会强加任何一个约束，因此它会一直搜索下去。

让我们逐步执行一个更简单的查询，(run 2 [q] (reverso [1] q))。

我们测试l和r是否都为空
它们不是，所以我们更新一些变量并断言 (conso la ld [1])
1. 成功，绑定 (== la 1) 和 (== ld [])。
接下来我们断言(appendo ldr [1] r)。
1. 这通过 appendo 中的第一个子句成功，绑定 (== ldr []) 和 (== r [1])。
我们递归到(reverso [] [])，并检查两个参数是否为空。
1. 这成功了，所以我们得到第一个总体结果：(== q [1])（记住在外层 (== q r)，所以 r 的解决方案是 q).
2. 我们被要求提供更多结果，所以我们继续搜索，这意味着拒绝刚刚成功的子句，看看替代方案是否会产生更多的成功。
  1. 拒绝 4.1 是一个很快的死胡同：此时我们有 (== l [])，所以 conso 失败了。
  2. 现在我们回到 3.1，(appendo ldr [1] r) 中的空列表子句。拒绝这一点会使我们进入第二个子句 (appendo d [1] r1)，绑定 (== ldr [a . d]) 和 (== r1 [a . r]).

你可以看到这永远不会导致任何结果：我们正在查看的列表比我们试图反转的列表要长。但在失败之前，它将再次递归调用 reverso，这将调用 appendo，这将再次延长列表并递归调用 reverso，并且很快。这是一个与 Goal ordering in Clojure's `core.logic`.

中描述的问题类似的问题

您可以通过首先通知引擎您希望两个列表的长度相同来解决此问题。然后 appendo 尝试将其输入和输出延长到超出限制的范围将会失败。首先，定义 same-lengtho:

(defn same-lengtho [xs ys]
  (conde
   [(== xs ()) (== ys ())]
   [(fresh [x xs' y ys']
      (conso x xs' xs)
      (conso y ys' ys)
      (same-lengtho xs' ys'))]))

然后在开始主搜索之前插入对 same-lengtho 的调用¹:

(defn reverso* [l r]
  (conde
   [(== l ()) (== r ())]
   [(fresh [la ld ldr]
      (conso la ld l)
      (appendo ldr (list la) r)
      (reverso* ld ldr))]))

(defn reverso [l r]
  (all (same-lengtho l r)
       (reverso* l r)))

如此定义，run* 查询会产生正确的结果，而不管参数顺序如何：

user=> (run* [q] (reverso q [1 2 3]))
((3 2 1))
user=> (run* [q] (reverso [1 2 3] q))
((3 2 1))

并且只是为了表明我们没有意外地用 same-lengtho 进行单向操作，请注意，在两边都有全新的变量的情况下，它仍然会生成所有可能的列表及其反转：

user=> (run 5 [a b] (reverso a b))
([() ()]
 [(_0) (_0)]
 [(_0 _1) (_1 _0)] 
 [(_0 _1 _2) (_2 _1 _0)] 
 [(_0 _1 _2 _3) (_3 _2 _1 _0)])

¹ 从技术上讲，您不再需要 (== l ()) 和 (== r ())：其中一个就足够了，因为您预先保证列表是一样的长度。但对我来说，保留冗余检查在语义上似乎更好。

查询变量在特定位置时不终止

Non-termination when query variable is on a specific position

clojure

logic-programming

minikanren

clojure-core.logic