prolog - NU-Prolog 和 Gödel 的逻辑和声音 `if-then-else` 扩展

Question

关于 paper 的 mercury 说明如下:

The if-then-else and negation constructs in most variants of Prolog are non-logical and unsound: they can cause the system to compute answers which are inconsistent with the program viewed as a logical theory. Some existing logic programming systems such as NU-Prolog and Gödel provide logical and sound replacements for these Prolog constructs. Unfortunately, these systems enforce safety via runtime groundness checks. This effect can increase the runtime of a program by an arbitrarily large factor; if the goals checked for groundness include large terms, the checks can be prohibitively expensive.

NU-Prolog 和 Gödel 看起来相当死气沉沉且不自由，但我仍然想知道:

这些合乎逻辑且合理的 if-then-else 替换是什么？

他们在 SWI 或 GNU Prologs 中有类似物吗？

它们是如何工作的？他们怎么能工作？在 Prolog 中添加逻辑否定会将其变成一般的 FOL，对吗？您基本上需要一个通用的 FOL 定理证明器来使用它？

它们与 if_/3 不同吗？ if_/3 必须扩展才能在新条件下使用。在 NU-Prolog 和 Gödel 中也必须这样做吗？

Answer 1

if-then-else 的突破可能是一个新的注释。
通过注释我理解模式声明之类的东西，
确定性声明等。对于 if then else，a
完整的声明会很好。假设我们可以
声明谓词或内置 p/n 完成。这个会
意味着它具有基本参数 t1,..,tn 的属性:

   T |- p(t1,..,tn)

- or -

   T |- ~p(t1,..,tn)

或者简而言之，如果理论 T 是递归可枚举的，那么它将是一个可判定的谓词。如果我们再记忆一下 if-then-else 在逻辑上是:

    ITE(A,B,C) == (A => B) & (~A => C)

然后我们可以使用完整的注释，如下所示。让我们
假设 A = p(t1,..,tn)。由于注释的Prolog
系统会尝试证明 A。如果它不成功，因为
Prolog 系统可以推断出完整的注释
〜A会成功。因此它可以使用 else 分支
没有~A的证明尝试。
但有趣的是，这已经是 ISO 核心
标准 if-then-else 确实， (A->B;C) 也只证明
一次。所以有什么问题？我想问题是
A 可能更复杂，不一定是基础。
甚至谓词 p/n 可能不完整，或者
我们甚至不知道它是否完整。总而言之
在这些情况下，ISO 核心标准仍然允许
我们使用 (A->B;C)。
接地问题有时可以通过使用运行时来解决
接地检查。这可能是水星所指的:

    when(ground(A), (A->B;C))

SWI-Prolog 甚至应用了一个技巧来制作接地气
查看更便​​宜，另见更多 discussion关于话语:

%!  trigger_ground(@Term, :Goal)
%
%   Trigger Goal when Term becomes   ground.  The current implementation
%   uses nonground/2, waiting for an   atribtrary  variable and re-check
%   Term  when  this  variable   is    bound.   Previous   version  used
%   term_variables and suspended  on  a   term  constructed  from  these
%   variables. It is clear  that  either   approach  performs  better on
%   certain types of terms. The term_variables/2  based approach wins on
%   large terms that are almost  ground.   Possibly  we need a nonground
%   that also returns the number of tests   performed  and switch to the
%   term_variables/2 based approach if this becomes large.

trigger_ground(X, Goal) :-
    (   nonground(X, V)
    ->  '$suspend'(V, when, trigger_ground(X, Goal))
    ;   call(Goal)
).