虚假的不等式约束

Question

报告者：Will Byrd

`
(is (=

 (run* [q]
   (fresh [x y]
     (!= (list x y) q)))
 ;; Simplified answer should just be:
 ;;
 ;; (_0)
 ;;
 ;; There is no way to violate this constraint, since neither
 ;; _1 nor _2 is reified. Both would need to be reified to be
 ;; able to violate the constraint.
 '((_0 :- (!= (_0 (_1 _2)))))))

`

我在这里提供一个建议的修复方法： https://github.com/clojure/core.logic/compare/master...namin:fix-for-meta?expand=1
但可能需要确保来自 mk 的其他测试用例也能按预期工作。

Will Byrd 建议将此测试文件转换为：
https://github.com/webyrd/faster-miniKanren/blob/master/disequality-tests.scm

Answer 1

评论由：namin 提出

有 9 个失败案例，分为 4 类（按重要性排序）
1. 被包含的约束
(!= (_1 6) (_0 5)) 被包含在 (!= (_0 5)) 中，因此如果后一个存在，应该删除前者。
2. 可简化的约束
(!= ((link: _0 1) (link: 5 1))) 应简化为 (!= _0 5)。
3. 冗余对称约束
(!= (_1 _0)) 和 (!= (_0 _1)) 是冗余的，并且只应保留后者。
这是 1 的一个特殊情况。
4. 良好的重新排序
(!= (_1 _0)) 应更规范地显示为
(!= (_0 _1))，交换操作数的顺序，
(!= (_0 _4)) (!= (_0 3)) 应更规范地显示为
(!= (_0 _3)) (!= (_0 4))，交换约束。
这似乎不是很重要。

Answer 2

参考：https://clojure.atlassian.net/browse/LOGIC-186（namin 报告）