7

以下 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]))))

是否有避免此问题的通用解决方案或常见做法？

4

2 回答 2

8

以下是我的理解：

使用core.logic，您希望尽早减少搜索空间。如果将membero约束放在首位，则运行将从搜索空间开始，并在约束membero产生的失败时回溯。==但是这个membero空间是巨大的，因为既不统一q也不x统一，或者至少是有界的。

但是如果你把==约束放在第一位，你直接x与统一[1 2 3]，现在的搜索空间membero显然与 的元素有界限x。

于 2013-01-13T21:01:56.123 回答
3

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

可以使用约束基础结构在更新版本的 core.logic中编写更好的版本membero，但是如何做到这一点的细节可能会在未来几个月内发生变化。直到有一个可靠的公共 api 来定义约束，你才会陷入困扰 Prolog 的那种微妙的排序和非终止问题。

于 2013-01-13T23:50:44.937 回答