clojure - 理解 core.logic !=

Question

我希望以下表达式返回许多结果，每个结果都由两个 cons 单元格组成，其中两个 cons 单元格不等价。但是，它返回 0 个结果。为什么我没有结果？

(run* [c1 c2] 
  (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2])
    (== ly [4 5])
    (membero x1 lx)
    (membero x2 lx) 
    (membero y1 ly)
    (membero y2 ly)
    (conso x1 y1 c1)
    (conso x2 y2 c2)
    (!= c1 c2)))

预期结果示例：

• [(1 . 4) (2 . 5)]
• [(1 . 4) (1 . 5)]
• [(2 . 4) (2 . 5)]

我不希望它返回像[(1 . 4) (1 . 4)]每个缺点中的两个点都相等的结果。

如果我删除该(!= c1 c2)部分，我会得到 16 个结果，包括两个缺点相同的结果。

如果替换为，我会得到预期的结果(!= c1 c2)：

(conde
  ((!= x1 x2))
  ((!= y1 y2)))

它应该做同样的事情，但明确检查两个单元格。

Answer 1

这不是一个有效的 core.logic 程序。你不能conso在尾巴不合适的地方使用。Scheme 中的 miniKanren 将允许您执行此操作，但 core.logic 的行为未定义。我已经修改了文档字符串conso以反映这一点。一个工作程序：

(run* [c1 c2] 
  (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2])
    (== ly [4 5])
    (membero x1 lx)
    (membero x2 lx) 
    (membero y1 ly)
    (membero y2 ly)
    (== [x1 y1] c1)
    (== [x2 y2] c2)
    (!= c1 c2)))

Answer 2

说你不能像这样使用 conso 的海报是正确的。这是文档字符串：

l 是一个集合的关系，其中 a 是 l 的第一个
，d 是 l 的其余部分。如果接地 d 必须绑定到正确的尾部。

您应该使用(== [x1 y1] c1)and(== [x2 y2] c2)或(conso x1 [y1] c1)and制作正确的列表(conso x2 [y2] c2)。