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)
).