compilation - 现代 Prolog 编译器是否会在安全的情况下自动优化发生检查？

Question

编辑：这个问题假设您启用了发生检查。这与设置 Prolog 标志无关。

30 年前有一堆关于自动优化发生检查的论文，当它是安全的时（大约 90% 的谓词，在典型的代码库中）。提出了不同的算法。现代 Prolog 编译器（例如 SWI Prolog）是否会做类似的事情（当发生检查打开时）？他们喜欢什么算法？

例如，他们会在编译这样的谓词时删除发生检查：

less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).

（来自这个答案下面的讨论）

Answer 1

当发生检查标志设置为“真”时，有多种优化可以优化发生检查。这对于使健全的统一适用于常见情况是必要的。典型的优化是检测头部的线性度：

linear(Head) :-
   term_variables(Head, Vars),
   term_singletons(Head, Singletons),
   Vars == Singletons.

在这种情况下，调用子句时可以省略发生检查。我们可以对这个less/2例子进行测试，头部是否是线性的。事实证明，两个头都是线性的：

?- linear(less(0, s(_))).
true.

?- linear(less(s(X), s(Y))).
true.

因此，Prolog 系统可以完全省略谓词的发生检查，less/2但仍能产生合理的统一。例如，在检查中间代码时，可以在 Jekejeke Prolog 中看到这种优化。使用指令 unify_linear：

?- vm_list(less/2).

less(0, s(A)).
  0  unify_linear _0, 0
  1  unify_linear _1, s(A)
less(s(X), s(Y)) :-
   less(X, Y).
  0  unify_linear _0, s(X)
  1  unify_linear _1, s(Y)
  2  goal_last less(X, Y)

与指令 unify_term 相比，指令 unify_linear 不执行发生检查，即使发生检查标志设置为真。

丽图查达；大卫 A. Plaisted (1994)。“在序言中没有发生检查的统一正确性”。逻辑编程杂志。18（2）：99-122。doi:10.1016/0743-1066(94)90048-5。

Answer 2

SWI Prolog 不会打开发生检查，除非您特别要求它：

• 通过使用unify_with_occurs_check/2而不是=本地。（请注意，这意味着头部统一不受影响，即仍然运行没有发生检查 - 我认为？）
• 通过设置标志进行全局occurs_check检查：set_prolog_flag(occurs_check,true)

这是一个问题吗？我不这么认为。

考虑在其他编程语言中使用断言的相关案例（甚至在 Prolog 中：assertion/1，我衷心推荐它）。

当您开发时，您将在运行时以一些 CPU 成本“打开”这些约束来验证约束。一旦您确定您的程序可以正常工作（通过构建、配置和测试），您将“关闭它们”。您的程序和任何调用者（可能是恶意的、混淆的或有问题的）之间的接口仍可能受到must_be/2检查的保护，以便强制执行接口契约。

发生检查的情况类似：如果您怀疑循环数据结构可能会出现并导致问题，请打开“发生检查”。您编写的代码使一切正常（并且您确定它正常工作，最好通过构造和证明）。然后再次将其关闭。

Answer 3

什么也很流行，使用变量内部的区别，如“新鲜”和“陈旧”变量。“新鲜”变量通常不需要发生检查。

可以动态地进行区分。下面是一些结果，动态区分（“新鲜度”）也可以结合一些静态分析（“线性”）：

上图显示了基于引用计数的启发式结果。下面的论文讨论了使用一位，即将变量标记为 UNBOUND 或 NEW_UNBOUND。

重新审视 Occur-Check 问题 - 啤酒，1988
https://core.ac.uk/download/pdf/82747799.pdf