SWI Prolog 中的约束处理规则："constraint store"是否仅在顶层目标处理期间存在？

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_contraint/1应该从约束存储中获取数据，但一旦chr程序运行，它就不会返回任何结果。因为不再有约束存储。

此外，试图在"CHR程序"中设置约束存储本身毫无意义。因此，将CCD_ 2放入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教程。一些注意事项：

CHR约束存储在哪里

在上面的教程中，在5下面哪个规则触发？我们读到：

当CHR处于静止状态时，没有任何约束处于活动状态。当我们呼叫来自Prolog的chr_contraint，它被添加并处于活动状态限制如果该规则导致添加其他规则，则它们将是活动约束。仅包含活动检查约束。

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

并且在6.1线程下

CHR存储是一个线程的本地存储。

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

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

Falco Nogatz的CHR约束服务器是一个有用的工具。

对于使用CHR的服务器来说，3只小猪游戏是一个有用的入门游戏因为它的逻辑。

Pengine会有自己的线索。这对CHR非常有用。

SWI Prolog文档称在全局变量下

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

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

回溯是怎么回事

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

如果任何规则主体中的Prolog失败，则对存储的所有更改由于最初尝试添加约束(通过从Prolog)被回滚。Prolog本身就没有做到这一点。