8

它们存在吗？它们是如何实施的？

SWI-Prolog的协程谓词（freeze,when等dif）具有警卫的功能。它们如何适应首选的 Prolog 编程风格？

我对逻辑编程非常陌生（使用 Prolog 和全部），并且对它不是纯粹的声明性这一事实感到有些困惑，即使在非常简单的情况下也需要程序考虑（请参阅有关使用\==ordif的这个问题）。我错过了什么重要的东西吗？

4

3 回答 3

5

首先是一个术语问题：在任何情况下，既不freeze/2也不when/2也不dif/2被称为警卫。Guards 出现在CHR等扩展中，或GHC（日文链接）或其他并发逻辑编程语言等相关语言中；您甚至（在某些限制下）可能会考虑以下形式的条款

:-护头, !,...

在这种情况下，包含警卫和剪切的子句将被称为提交。但没有一个适用于上述原语。Guards 的灵感来自 Dijkstra 1975 年的Guarded Command Language。

freeze(X, Goal)（最初称为geler）与 相同，when(nonvar(X), Goal)并且它们在声明上都等同于Goal. 与守卫的功能没有直接关系。但是，当与 if-then-else 一起使用时，您可能会实现这样的保护。但那是完全不同的。

freeze/2一段时间以来，类似的结构被认为是改进 Prolog 执行机制的一般方法。然而，事实证明它们使用起来非常脆弱。通常，他们过于保守，从而不必要地延迟了目标。也就是说，几乎每个有趣的查询都会产生一个“挣扎”的答案，如下面的查询。此外，终止程序和非终止程序之间的界限现在要复杂得多。对于终止的纯单调 Prolog 程序，在程序中添加一些终止目标将保留整​​个程序的终止。但是，freeze/2情况不再如此。那么从概念上来说，freeze/2没有得到顶层系统的很好支持：只有少数系统以全面的方式（例如 SICStus）显示了延迟目标，这对于理解成功/答案和解决方案之间的区别至关重要。随着延迟的目标，Prolog 现在可能会产生一个没有解决方案的答案：

?- 冻结（X，X = 1），冻结（X，X = 2）。
冻结（X，X=1），
冻结（X，X=2）。

另一个困难freeze/2是终止条件更难确定。因此，虽然freeze应该解决终止的所有问题，但它经常会产生新的问题。

还有更多的技术困难与freeze/2特别是 wrt 表和其他防止循环的技术有关。freeze(X, Y = 1)清楚地考虑一个目标，Y现在1即使它还没有被绑定，它仍然在等待X首先被绑定。现在，一个实现可能会考虑为一个目标制定表g(Y)。g(Y)现在要么没有解决方案，要么只有一个解决方案Y = 1。这个结果现在将作为唯一的解决方案存储，g/1 因为freeze-goal 对目标不直接可见。

正是由于这些原因，freeze/2才被认为是约束逻辑编程的首选。

另一个问题是dif/2今天被认为是一个约束。与freeze/2其他协同程序原语相比，约束能够更好地管理一致性并保持更好的终止属性。这主要是因为约束引入了定义明确的语言，具体属性可以得到证明，并且已经开发了特定的算法并且不允许一般目标。然而，即使对他们来说，也有可能获得不是解决方案的答案。更多关于CLP 中的答案和成功。

于 2012-12-08T20:39:26.507 回答
4

freeze/2 和 when/2 就像逻辑编程的“goto”。它们不是纯的、可交换的等。

另一方面，dif/2 是完全纯的和声明性的、单调的、可交换的等。dif/2 是一个声明性谓词，如果它的参数不同，它就成立。至于“首选的 Prolog 编程风格”：说明什么是成立的。如果要表达两个通用术语不同的约束，则 dif/2 正是说明了这一点。

当您不在 Prolog 的纯声明性子集中编程时，通常最需要程序考虑，而是使用不可交换的不纯谓词等。在现代 Prolog 系统中，几乎没有理由离开纯声明性子集。

于 2012-12-07T09:23:29.613 回答
0

Evan Tick 有一篇论文解释了 CC：

非正式地，过程调用通过匹配头参数（被动统一）并满足保护目标来提交子句。当一个目标可以在一个程序中提交多个子句时，它会不确定地提交其中一个子句（其他候选者被丢弃）。如果目标的相应参数没有充分实例化，则出现在子句的头部和保护中的结构会导致执行暂停。当与挂起的调用关联的变量充分实例化时，可以稍后恢复挂起的调用。

并发逻辑编程语言的演变
Evan Tick - 1995
https://core.ac.uk/download/pdf/82787481.pdf

所以我猜想通过一些 when/2 的魔法，一个提交的选择代码可以被重写为普通的 Prolog。方法如下。对于同一谓词的一组提交选择规则：

H1 :- G1 | B1.
...
H2 :- Gn | Bn.

这可以改写成下面的形式，其中 Hi' 和 Gi' 需要实现被动统一。例如，通过使用 ISO 更正 subsumes_term/2。

H1' :- G1', !, B1.
..
H1' :- Gn', !, Bn.
H :- term_variables(H, L), when_nonvar(L, H).

上述翻译不适用于 CHR，因为 CHR 不会丢弃候选人。

于 2018-11-04T02:20:27.477 回答