Clojure的`core.logic`中的目标排序

Question

以下Clojure代码用于core.logic在两个不同的顺序中解决具有相同目标的相同逻辑问题.这种订购选择导致一个快速完成而另一个挂起.

(use `clojure.core.logic)

;; Runs quickly.  Prints (1 2 3).
(clojure.pprint/pprint (run* [q] (fresh [x] (== x [1,2,3]) 
                                            (membero q x))))

;; Hangs
(clojure.pprint/pprint (run* [q] (fresh [x] (membero q x) 
                                            (== x [1,2,3]))))

是否有一般解决方案或通常的做法来避免这个问题？

Answer 1

这是我的理解:

有了core.logic,您希望尽早减少搜索空间.如果首先放置membero约束,则运行将通过搜索membero空间开始,并回溯==约束产生的失败.但这个membero空间是巨大的,因为它既q不是x统一的,也不是至少是有限的.

但是如果你把==约束放在第一位,就直接统一x了[1 2 3],而membero现在的搜索空间显然与元素有关x.

Answer 2

如果您要使用membero此问题，则没有通用的解决方案。使用新的变量调用membero将导致它生成所有（读取，无限）可能的列表，该列表q是其成员。当然，大于 3 的列表不适用 - 但既然您已经使用过，run*它将继续盲目地尝试大于 3 的列表，即使每个列表都会失败。

可以membero使用约束基础设施在较新版本的 core.logic 中编写更好的版本，但如何实现这一点的细节可能会在未来几个月内发生变化。在有一个可靠的公共 API 来定义约束之前，您会遇到困扰 Prolog 的微妙排序和非终止问题。