NU-Prolog 和 Gödel 的逻辑和合理的“if-then-else"扩展 [英] NU-Prolog's and Gödel's logical and sound `if-then-else` extension

问题描述

关于论文mercury" class="post-tag" title="show questions tagged 'mercury'" rel="tag">mercury 说明如下:

A paper about mercury says the following:

大多数 Prolog 变体中的 if-then-else 和否定结构都是不合逻辑且不合理的:它们会导致系统计算与被视为逻辑理论的程序不一致的答案.一些现有的逻辑编程系统，例如 NU-Prolog 和 Gödel，为这些 Prolog 结构提供了逻辑和合理的替代.不幸的是，这些系统通过运行时基础检查来加强安全性.这种效果可以将程序的运行时间增加任意大的系数；如果检查基础性的目标包含大量条款，则检查费用可能会高得令人望而却步.

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 看起来相当死和不自由，但我仍然想知道:

NU-Prolog and Gödel look rather dead and non-free, but I still wonder:

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

• What are these logical and sound if-then-else replacements?
• Do they have analogs in SWI or GNU Prologs?
• How do they work? How could they work? Adding logical negation to Prolog turns it into general FOL, right? You would basically need a general FOL theorem prover to work with it?
• Are they different from if_/3? if_/3 has to be extended to be used with new conditions. Would one have to do this in NU-Prolog and Gödel also?

推荐答案

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

A break through in if-then-else could be a new annotation. By annotation I understand things like mode declarations, determinancy declarations, etc.. For an if then else, a complete declaration would be nice. Lets assume we could declare a predicate or built-in p/n complete. This would mean it has the property for ground arguments t1,..,tn:

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

- or -

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

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

Or in short it would be a decidable predicate if the theory T is recursively enumerable. If we then recall that if-then-else is logically:

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

然后我们可以使用完整的注释如下.让我们假设 A = p(t1,..,tn).由于注释Prolog系统会尝试证明 A.如果它不成功，因为在完整的注释中，Prolog 系统可以推断出~A 会成功.因此它可以使用 else 分支没有~A的证明尝试.

We could then use the complete annotation as follows. Lets assume A = p(t1,..,tn). Because of the annotation the Prolog system would try to prove A. If it doesn't succeed, because of the complete annotation, the Prolog system can infer that ~A would succeed. And therefore it can use the else branch without a proof attempt of ~A.

但有趣的是，这已经是 ISO 核心标准的 if-then-else 确实如此，(A->B;C) 也仅证明一次.所以有什么问题?我想问题是A 可能更复杂，不一定是接地的.甚至谓词 p/n 可能不完整，或者我们甚至不知道它是否完整.总而言之在这些情况下，ISO 核心标准仍然允许我们使用 (A->B;C).

But interestingly this is already what the ISO core standard if-then-else does, (A->B;C) does also only prove A once. So whats the problem? I guess the problem is that A might be more complex and not necessarily ground. Or even that a predicate p/n might be incomplete, or we even don't know whether it is complete. And in all these cases the ISO core standard nevertheless allows us to use the (A->B;C).

groundness 问题有时可以通过使用运行时来解决基础检查.这可能就是 Mercury 所指的:

The groundness problem can sometimes be solved by using a runtime groundness checks. This is probably what Mercury refers to:

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

SWI-Prolog 甚至应用了一个技巧来制作基础检查更便宜，另见一些进一步的讨论 关于话语:

SWI-Prolog even applies a trick to make the groundness check cheaper, see also some further discussion on 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)
).

这篇关于NU-Prolog 和 Gödel 的逻辑和合理的“if-then-else"扩展的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！