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

Posted 2023-05-08

【中文标题】现代 Prolog 编译器是不是会在安全的情况下自动优化发生检查？

【英文标题】：Do modern Prolog compilers optimize away the occurs check automatically, when it's safe?现代 Prolog 编译器是否会在安全的情况下自动优化发生检查？

【发布时间】：2021-03-24 15:41:01

【问题描述】：

编辑： 这个问题假设您启用了发生检查。 不是关于setting Prolog flags。

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

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

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

（来自下面的讨论this answer）

【问题讨论】：

SWI-Prolog 不会自行更改 ISO 标志。在plunit library docs，sto(Terms) 部分，建议See 7.3.3 of ISO/IEC 13211-1 PROLOG: Part 1 - General Core, for a detailed discussion of STO and NSTO

【参考方案1】：

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

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.

【参考方案2】：

除非您明确要求，否则 SWI Prolog 不会打开发生检查：

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

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

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

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

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

【讨论】：

问题假设发生检查是打开的，当然（否则，没有什么可以删除）：“（当发生检查打开时）？”

@MaxB Aie... 来晚了。

【参考方案3】：

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

可以动态进行区分。下面是一些结果，动态区分（“Freshness”）也可以结合一些静态分析（“Linear”）：

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

再访 Occur-Check 问题 - Beer，1988 年https://core.ac.uk/download/pdf/82747799.pdf