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

Question

我正在仔细研究约束处理规则(CHR)，看看我是否能理解它们（从某种意义上说，这里计算的是什么以及经典逻辑甚至线性逻辑如何适合于此）并可能应用它们。

Thom Frühwirth 2009 年的书讨论了 CHR 的原则，但实施当然可能有所不同。

在这种情况下，我使用CHR的SWI Prolog 实现。

如果我理解得很好：

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