SWI Prolog 中的约束处理规则：“约束存储”是否仅在顶级目标处理期间存在？

Question

我正在仔细研究Constraint Handling Rules (CHR)，看看我是否能理解它们（从某种意义上说，这里计算的是什么，经典逻辑甚至linear logic 是如何适应这个的）并可能应用它们。

Thom Frühwirth's book 从 2009 年开始讨论 CHR 的原则，但实现当然可能不同。

在这种情况下，我使用的是SWI Prolog implementation of CHR。

如果我理解得很好：

1. CHR 的实现将提供至少一个“约束存储”来表达“计算的状态”。约束存储仅包含基本原子（即正字面量）。
2. 在典型的 CHR 会话中，首先设置具有初始状态的约束存储。一个人编写 CHR 程序，其中包含 CHR 规则。然后以约束存储作为参数运行 CHR 程序。重复应用正向链接 CHR 规则直到不再有任何规则适用，这将迭代地（并且破坏性地）将约束存储从其初始状态转换为某个最终状态。然后可以检查约束存储以找到所需的答案。
3. 在这种情况下，只考虑不关心非确定性（“承诺选择非确定性”）：当多个规则适用于任何中间状态时，将采用任何规则。
4. 不考虑在以后失败的情况下回溯到选择点的“不知道”非确定性 - 由实现以一种或另一种方式提供这一点，如果需要的话。

作为一个练习，一个使用欧几里得算法计算 GCD 并保留操作日志的最简单程序：

% Constraint `logg(Ti,Msg)` retains the log message `Msg` at step `Ti`
% (which increases monotonically)
% Constraint `gcdpool(X)` denotes a "GCD pool member". At each step, we want
% to compute the GCD of all the X for which there is a `gcdpool(X)` constraint
% in the constraint store. A CHR transformation of the store always reduces the
% sum of the X (variant) while keeping the GCD of the GCD pool members constant
% (invariant). We will thus find a solution eventually.

:- module(my_gcd, [  gcdpool/1, logg/2 ]).
:- use_module(library(chr)).

:- chr_constraint gcdpool/1, logg/2.

% pool contains duplicate: drop one! 

gcdpool(N) \ gcdpool(N),logg(Ti,Msg) <=> To is Ti+1, logg(To,[[drop,[N,N],[N]]|Msg]).

% pool contains 1 and anything not 1: keep only 1

gcdpool(1) \ gcdpool(N),logg(Ti,Msg) <=> 1<N | To is Ti+1, logg(To,[[drop,[1,N],[N]]|Msg]).

% otherwise

gcdpool(N) \ gcdpool(M),logg(Ti,Msg) <=> 0<N, N<M | To is Ti+1, 
                                                    V is M-N, 
                                                    gcdpool(V), 
                                                    logg(To,[[diff,[N,M],[N,V]]|Msg]).

这一切都非常简单。在 SWI Prolog 中运行测试

?- use_module(library(chr)).
?- [gcd].
?- chr_trace.
% now we enter a goal:
?- gcdpool(6),gcdpool(3),logg(0,[]).
CHR:   (0) Insert: gcdpool(6) # <907>
CHR:   (1) Call: gcdpool(6) # <907> ? [creep]
CHR:   (1) Exit: gcdpool(6) # <907> ? [creep]
CHR:   (0) Insert: gcdpool(3) # <908>
CHR:   (1) Call: gcdpool(3) # <908> ? [creep]
CHR:   (1) Exit: gcdpool(3) # <908> ? [creep]
CHR:   (0) Insert: logg(0,[]) # <909>
CHR:   (1) Call: logg(0,[]) # <909> ? [creep]
CHR:   (1) Try: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]).
CHR:   (1) Apply: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]). ? [creep]
CHR:   (1) Remove: gcdpool(6) # <907>
CHR:   (1) Remove: logg(0,[]) # <909>
CHR:   (1) Insert: gcdpool(3) # <910>
CHR:   (2) Call: gcdpool(3) # <910> ? [creep]
CHR:   (2) Exit: gcdpool(3) # <910> ? [creep]
CHR:   (1) Insert: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR:   (2) Call: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR:   (2) Try: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]).
CHR:   (2) Apply: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]). ? [creep]
CHR:   (2) Remove: gcdpool(3) # <910>
CHR:   (2) Remove: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR:   (2) Insert: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912>
CHR:   (3) Call: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR:   (3) Exit: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR:   (2) Exit: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR:   (1) Exit: logg(0,[]) # <909> ? [creep]

gcdpool(3),
logg(2, [[drop, [3, 3], [3]], [diff, [3, 6], [3, 3]]]) .

答案由最后两行给出：约束存储中唯一剩下的约束是gcdpool(3)，所以答案是3。

在实施方面，以下似乎成立：

没有专门的“约束存储”。 CHR 程序（以某种方式）被编译到 Prolog 中，并且“CHR 约束”成为“Prolog 谓词”。这样的“约束存储”是称为 Prolog 顶级目标的堆栈（它没有被具体化）。

因此，“约束存储”使用“CHR 目标”中列出的约束进行初始化，并在最终退出时消失。您也不能以逐步或交互的方式设置约束存储，但必须在一行中完成：

gcdpool(6),gcdpool(3),logg(0,[]).

之后，CHR 程序立即开始工作。

确实，谓词find_chr_constraint/1 应该从约束存储中获取数据，一旦CHR 程序运行，它什么也不返回。因为没有约束存储了。

此外，尝试在“CHR 程序”本身中设置约束存储是没有意义的。因此将logg(0,[]) 放入GCD 代码没有任何效果。您必须将logg(0,[]) 放入CHR 目标中。

问题

• 这种理解正确吗？
• 如何将 CHR 计算结果返回到 Prolog？
• 如何处理 Prolog 实现提供的回溯可能性？如何将其用于 CHR？

Answer 1

关于“如何将 CHR 计算结果返回到 Prolog？”。

你可以这样做：

:- chr_constraint item/1, get_item/1.

item(In) \ get_item(Out) <=> In = Out.

查询：

?- item(foo),get_item(X).
X = foo.

查看本教程了解更多信息：http://www.pathwayslms.com/swipltuts/chr/index.html

Answer 2

我正在关注 Anne Ogborn 的 CHR tutorial。一些注意事项：

CHR 约束存储在哪里？

在上面的教程中，5 Which Rule fires? 下我们读到：

当 CHR 只是坐在那里时，没有任何约束处于活动状态。当我们调用 来自 Prolog 的 chr_constraint，它被添加并激活 约束。如果该规则导致添加其他规则，则依次它们 将是主动约束。仅包含活动的规则 检查约束。

这使商店更加稳定。你不必担心一些 触发规则的无关操作。

在6.1 Threads下

CHR 存储对于一个线程来说是本地的。

这在实现使用 CHR 的服务器时尤其痛苦。

一种解决方案是在一个特殊线程上完成所有 CHR 工作。

Falco Nogatz 的 CHR-Constraint-Server 是一个有用的工具。

3 Little Pigs 游戏对于使用 CHR 的服务器来说是一个有用的启动器 因为它的逻辑。

Pengine 将有自己的线程。这对 CHR 很有用。

SWI Prolog 文档在global variables 下说

全局变量是名称（原子）和术语之间的关联。 它们与使用 assert/1 或 记录/3。

值存在于 Prolog（全局）堆栈中。这意味着查找 时间与术语的大小无关。这尤其 对大型数据结构感兴趣，例如已解析的 XML 文档或 CHR 全局约束存储。

回溯是怎么回事？

CHR 规则不会回溯，因为该概念在 CHR 方法中毫无意义。然而，在Making CHR interact with Prolog 下，我们读到：

如果任何规则正文中的 Prolog 失败，则对存储的所有更改 由于最初尝试添加约束（通过从 Prolog) 被回滚。然后，Prolog 本身就失败了。