1

考虑这篇博文，作者使用以下方法实现回文关系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程序没有终止？
4

1 回答 1

2

问题是，当您appendo在左侧给出一个新变量并为结果提供一个新变量时，它可以产生任意多个答案，但没有一个会导致您的整个reverso问题的解决方案。见证的定义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)).

  1. 我们测试是否l和r都是空的
  2. 他们不是，所以我们更新了一些变量并断言(conso la ld [1])
    1. 这成功了，绑定(== la 1)和(== ld []).
  3. 接下来我们断言(appendo ldr [1] r).
    1. appendo这通过绑定(== ldr [])和中的第一个子句成功(== r [1])。
  4. 我们递归到(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，依此类推。这与 Clojure 的 `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然后在开始主搜索之前插入调用1：

(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)])

1(== l ())从技术上讲，您不再需要两者(== r ())：任何一个都足够了，因为您预先保证列表的长度相同。但对我来说，留在冗余检查中似乎在语义上更好。

于 2021-11-29T22:24:40.017 回答