虚假不等式约束

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 报告)