我需要在某些 Prolog 问题中使用前向链接器。 我想避免使用普通的元解释器从头开始实现它（但如果没有其他选项可用，我将不得不这样做），因为使用元解释器执行此操作会很慢，而且我我确信应该有一些好的实现。 有人知道 YAP 或 SWI Prolog 是否包含原生且高效的前向链接器？如果是这种情况，将非常感谢您提供有关如何安装/使用它的指针。
如果这两个 Prolog 引擎上没有本地前向链接器可用，有人可以推荐我一个基于 vanilla 元解释器的好的开源实现，我可以将其用作外部 Prolog 库吗？
提前致谢。
【问题讨论】：
标签： prolog
YAP 和 SWI 都包含约束处理规则的实现 - http://dtai.cs.kuleuven.be/projects/CHR/ - 这是一个正向链接规则系统。
对于您的特定问题，我无法谈论它的性能，但众所周知 CHR 是有效的（请参阅从 CHR 网站链接的论文）。
CHR 还具有 Java、Haskell 和 C 实现，因此如果您以后需要更好的性能，您可以轻松地将规则移植到其中一种语言。
【讨论】：
:- use_module(library(chr)).
让我们根据最小逻辑而不是根据解析定理证明来解释后向链接和前向链接。正常的后向链接Prolog规则可以看作是最小逻辑左蕴涵引入规则的应用。所以基本上当我们有一个目标 P 和一个规则 A->P 时，组合推理规则说我们可以用目标 A 替换目标 P：
-------- (Id)
P |- P G, A -> P |- A
--------------------------------- (Left ->)
G, A -> P |- P
现在可以使用相同的规则来为正向链接应用程序建模。这次我们没有目标 P，而是在前提中实现了条件 A。当存在规则 A -> P 时，该规则也允许我们实现头部 P。组合推理规则如下：
------- (Id)
A |- A G, A, A -> P, P |- B
--------------------------------------- (Left ->)
G, A, A -> P |- B
我们这个小程序的想法是完全计算正向链接过程的固定点 F(M) = M。我们所做的是计算迭代 M0、M1、M2 等。仅当过程以有限结果终止时才有效。从演绎数据库中，我们采用了仅计算 Mn+1 和 Mn 之间的增量的想法。可以找到一个 G，使得 F(Mn)\Mn = G(Mn\Mn-1,Mn-1) 相对较少的努力。
当前 G 的实现可能会偶然发现循环数据，因为目前还没有消除重复数据。在还允许删除事实的前向链接器中，可以使用特殊的前向规则来消除重复项。成熟的前向链接系统无论如何都应该允许删除事实，然后它们甚至可以用于实现约束求解系统。
但是，让我们先把简单的想法和相应的简单代码放在一边。
F 函数的 G 函数 (delta/2)（原始规则）
http://www.xlog.ch/jekejeke/forward/delta.p
【讨论】：