clojure - 为什么 core.logic 的输出重复给出相同的值？

Question

我在 core.logic 中尝试过这个

(require [clojure.core.logic :as l])(l/run* [q]  (l/fresh [a b c]    (l/membero a [1])    (l/membero b [4 5])    (l/membero c [1 2])    (l/== q [a b])))

expecting the result to be [1 4] [1 5]

but it was [1 4] [1 4] [1 5] [1 5]

then I started playing with it and found this:

(require [clojure.core.logic :as l])(l/run* [q]  (l/fresh [a b c]    (l/membero a [1])    (l/membero b [4 5])    (l/membero c [1 1 1 1 1 1 1 1])    (l/== q [a b])))

 ;; => ([1 4] [1 4] [1 4] [1 5] [1 4] [1 4] [1 5] [1 4] [1 5] [1 4] [1 5] [1 5] [1 5] [1 5])

其中有一个 [1 5] 散布在 [1 4]

发生什么事了？这种重复的事情应该是一个功能还是一个错误？

Answer 1

这是因为逻辑变量c的使用不是必需的，因为它没有与q统一。如果删除 c 那么你将得到想要的结果。基本上，您需要了解 core.logic 中的替换是如何工作的，以了解为什么您会因为 c 而获得这些重复的结果。

在较高层次上，该过程就像在树中搜索解决方案，在这种情况下，向量中的每个元素(membero 和 c)都会指向搜索树，这会导致重复结果，因为对于 c 引入的每个节点，可能值会导致正确的结果，因为 c 未在统一中使用 (l/= = q [a b])