core.logic 统一匹配映射中的值但不匹配键答案

【问题标题】：core.logic unification matches value in map but not keycore.logic 统一匹配映射中的值但不匹配键
【发布时间】：2014-12-05 20:18:20
【问题描述】：

我不明白为什么从下面两个例子中，第一个返回正确的值(1)，而第二个返回()。我本来希望得到(:key) 的结果，或者是找不到解决方案的异常，但不是空列表。

(l/run* [q]
  (l/== {:key 1} {:key q}))

;; BUT IT DOESNT WORK

(l/run* [q]
  (l/== {:key 1} {q 1}))

【问题讨论】：

run* 返回解决方案列表，因此 () 表示没有解决方案
同意，但据我了解，有一个解决方案。如果你使用q = :key，那不满足方程吗？我认为我们必须将答案解读为：couldn't find a solution 而不是 I can guarantee that no solution exist。

【解决方案1】：

我没有发现它记录为预期的行为，但查看source code，根据我的（有限的）理解，地图的统一似乎只发生在值上，而不是键。

正如在unify-with-map* 中实现的那样，当core.logic 在第一个映射中找到键:key 时，它会在第二个映射中查找它的值，但没有找到它，因此放弃了统一。由于没有解决方案，就像@Arthur Ulfeldt 说的那样，你最终会得到()。

【讨论】：

在这种情况下限制core.logic？但是需要注意的一个好问题 ;) 我的感觉是，如果您扩展搜索空间以包含键，您可能需要做更多的工作，因此它可能与性能权衡有关。令我惊讶的是，core.logic 中的“没有解决方案”可能只是意味着它无法解决它，尽管存在解决方案。所以“没有解决方案”并不能保证。但它仍然非常强大，它可以统一值，这可能是你大多数时候都会使用的。
是的，这是正确的。映射键不能是 lvar。它可能没有太多的文档记录，但这就是该功能的设计方式。