时间戳

首页 > 解决方案 > SWI Prolog 中的约束处理规则：“约束存储”是否仅在顶级目标处理期间存在？

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

问题描述

我正在仔细研究约束处理规则（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目标。

问题

标签： prologconstraint-handling-rules

解决方案

关于“如何将 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

推荐阅读