2

一篇关于论文说:

Prolog 的大多数变体中的 if-then-else 和 negation 结构是不合逻辑且不合理的:它们会导致系统计算出与被视为逻辑理论的程序不一致的答案。一些现有的逻辑编程系统,例如NU-Prolog 和 Gödel 为这些 Prolog 结构提供了逻辑和合理的替代。不幸的是,这些系统通过运行时接地检查来强制执行安全性。这种效果可以将程序的运行时间增加任意大的倍数;如果检查基础的目标包括大项,则检查可能会非常昂贵。

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

  • 这些合乎逻辑且合理的if-then-else替代品是什么?
  • 他们在 SWI 或 GNU Prologs 中有类似物吗?
  • 它们是如何工作的?他们怎么工作?在 Prolog 中添加逻辑否定会将其变成一般的 FOL,对吗?您基本上需要一个通用的 FOL 定理证明器来使用它?
  • 它们与 不同if_/3吗?if_/3必须扩展以在新条件下使用。在 NU-Prolog 和 Gödel 中也必须这样做吗?
4

2 回答 2

1

if-then-else 的突破可能是一个新的注释。通过注释,我了解模式声明、确定性声明等。对于 if then else,完整的声明会很好。假设我们可以声明一个谓词或内置 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 一次。所以有什么问题?我想问题是 A 可能更复杂,不一定是基础。甚至谓词 p/n 可能不完整,或者我们甚至不知道它是否完整。在所有这些情况下,ISO 核心标准仍然允许我们使用 (A->B;C)。

接地问题有时可以通过使用运行时接地检查来解决。这可能是水星所指的:

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

SWI-Prolog 甚至应用了一个技巧来降低接地检查的成本,另请参阅 Discourse 上的一些进一步讨论

%!  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)
).
于 2020-12-22T02:02:35.107 回答
0

如果有人感兴趣,我在这里找到了 MU- 和 NU-Prologs 的这篇评论:

在此处输入图像描述

于 2020-12-25T03:37:12.587 回答