SWI Prolog中的约束处理规则：“约束存储”是否仅存在于toplevel目标处理的持续时间内？

Question

我正在仔细研究约束处理规则 (CHR)，看看我是否能够理解它们(从这个意义上讲，这里计算的是什么，古典逻辑，甚至线性逻辑是如何融入其中的)，并可能应用它们。

2009年的Thom Frühwirth书讨论了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 toplevel目标的堆栈(未具体化)。

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

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

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

实际上，谓词约束/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

我在跟踪安妮·奥格伯恩的伟大CHR教程。一些注意事项：

CHR约束存储在哪里？

在上面的教程中，在5哪条规则开火？下面我们看到：

当CHR只是坐在那里时，没有约束是活动的。当我们从Prolog调用一个chr_constraint时，会添加它并使其成为活动约束。如果该规则导致添加其他规则，则它们将成为活动约束。只检查包含活动约束的规则。 这使商店更加稳定。你不必担心一些无关的行为会触发规则。

以及在6.1线程下

CHR存储是一个线程的本地存储。 在实现使用CHR的服务器时，这特别痛苦。 一种解决方案是在一个特殊线程上完成所有的CHR工作。 Falco的CHR-约束服务器是一个有用的工具。 对于使用CHR作为逻辑的服务器来说，3只小猪游戏是一个有用的启动程序。 Pengine会有自己的线程。这对于CHR是有用的。

SWI文档显示在全局变量下

全局变量是名称(原子)和术语之间的关联。它们与使用assert/1或recorda/3存储信息的方式不同。 该值存在于Prolog (全局)堆栈上。这意味着查找时间与术语的大小无关。对于大型数据结构(如解析的XML文档或CHR全局约束存储)来说，这特别有趣。

回溯是怎么回事？

CHR规则不会倒退，因为这个概念在CHR方法中是没有意义的。然而，在使CHR与Prolog交互下，我们读到：

如果任何规则正文中的Prolog失败，则回滚自最初尝试添加约束(从Prolog调用)以来对存储的所有更改。Prolog本身就失败了。