为啥会返回这个矛盾的 clojure.core.logic/featurec 结果？

Posted 2023-05-08

【中文标题】为啥会返回这个矛盾的 clojure.core.logic/featurec 结果？

【英文标题】：Why is this contradictory clojure.core.logic/featurec result being returned?为什么会返回这个矛盾的 clojure.core.logic/featurec 结果？

【发布时间】：2015-11-15 13:24:26

【问题描述】：

...我该如何避免呢？

(run* [q]
   (featurec q :a 1)
   (featurec q :a 2)))

返回

((_0
  :-
  (clojure.core.logic/featurec _0 :a 2)
  (clojure.core.logic/featurec _0 :a 1)))

我理解这意味着_0 映射必须至少包含:a 1 键值对和:a 2 键值对。这似乎是矛盾的，因为:a 不能同时映射到1 和2，除非我们使用MultiMaps。我无法将其解读为:a 1 或:a 2，因为我指定的约束是连词。我原以为结果应该是()，因为约束是矛盾的； q 没有可以满足这些约束的值。

我一定是读错了结果。

【参考方案1】：

是的，这是矛盾的。但事实就是这样：没有任何地图可以同时与:a 1 和:a 2 统一。

run*、all、fresh 都在其约束中引入了一个连词 (AND)。如果你想要析取（OR），你可以引入conde。

也许您的问题是：为什么 core.logic 无法“看到”矛盾并返回空结果集？我不确切知道。但也许这与这样一个事实有关，即即使我们移除其中一个约束，我们也不会得到“接地”的结果：

(run* [q]
   (featurec q :a 1))

;=> ((_0 :- (clojure.core.logic/featurec _0 :a 1)))

它读作：任何东西，只要它是一个包含[:a 1] 条目的地图。我认为这是正确的结果。

【讨论】：

是的，我的问题正如你所说：“为什么 core.logic 不能“看到”矛盾并返回一个空的结果集？”

删除其中一个约束:a 2 得到的结果实际上对我来说非常有意义；正如你所说，这是正确的结果。任何包含条目:a 2 的地图都是有效的解决方案。但是，这并不能解释为什么在前面的示例中会返回矛盾。