prolog - Prolog中处理 "residual goals"的方法是什么？

Question

以这个程序为例。它使用延迟的目标

room(green).
room(blue).
room(red).
room(white).

location(jimmy,red).
location(ricky,blue).
location(cindy,green).

% "Is a certain room unoccupied?"
   
not_occupied(Room) :-
   nonvar(Room),
   assertion(room(Room)),
   \+ location(_Person,Room).

% If no specific "Room" has been given, the negated goal is
% delayed until the "Room" has been instantiated.

not_occupied(Room) :-
   var(Room),
   !,
   when(
      ground(Room),
      (\+ location(_Person,Room))
   ).

如果我现在问

?- not_occupied(R).

然后 Prolog 成功并输出一个残差目标

?- not_occupied(R).
when(ground(R),\+location(_7676,R)).

实际上，它并没有真正成功。它乐观地成功(因为为了不停止计算，它必须成功)但实际的逻辑成功取决于剩余目标的实际成功。
如何以编程方式确定子目标是否成功实现了剩余目标？ (那我该怎么办？)方法是什么？
附言
拥有第二个 Prolog 真值可能是一个不错的 Prolog 扩展，因为 true+将表示“在剩余目标成功的条件下成功”。这实际上似乎是有必要的:
在 SWI-Prolog 中，采用这个固有的模棱两可的目标:

do :- not_occupied(_).

调用它甚至根本不会打印出任何剩余目标:

?- do.
true.

目标成功了吗？不是真的，它仍然处于逻辑边缘，但顶层甚至没有告诉我。另一方面，没有办法向程序提供更多信息来解决剩余目标。但是因为计算运行到终点而默认为“成功”感觉是错误的。

Answer 1

首先是一些术语问题。我们从顶层得到的是一个答案。说:

?- length(Xs, 0).
   Xs = [].

在这里，答案是 的形式。答案替换 它描述了一个单一的解决方案。

?- length(Xs, 1).
   Xs = [_A].

同样，这是一个答案替换，但这次它描述了无限多的解决方案。
通常答案和解决方案的概念可以互换使用，但是一旦我们使用延迟的目标或约束，我们就需要明确区分。现在的新功能是答案可能包含任意数量的解决方案，甚至根本没有。

?- freeze(X, false).
   freeze(X,false).   % no solution

?- freeze(X, ( X = 1 ; X = 2 ) ).
   freeze(X,(X=1;X=2)).  % two solutions

一些实现提供 frozen(Var, Goal)只获得与 Var 相关的目标.在这种情况下，内置的 call_residue(Goal_0, Residuum)被构思出来。最初，在 SICStus 0.7 中，它是为延迟目标定义的，剩余的定义非常明确。然而，一旦我们将我们的语言扩展到 clpfd，事情就变得不那么清楚了。这是 SICStus 3.12.5:

| ?- X in 1..3, call_residue(X in 2..4, Residuum).
Residuum = [[X]-(X in 2..3),
X in 1..3 ?

现在的残渣应该是 X in 2..3或 X in \{1} ?事情可能变得相当复杂(阅读: buggy )。此外，撤消绑定(bind)是一项艰巨的任务。或实现首先创建整个目标的副本，然后保留约束。
SICStus 4 已替换 call_residue/2通过两个新的内置插件。 call_residue_vars(Goal_0, Vars)统一 Vars与在 Goal_0 中创建的延迟目标或约束相关的变量.请注意，当某些受约束的变量存在于 Goal_0 之前，这个概念并不那么精确。并出现在 Goal_0 .但主要的一点是，这个内置的实现起来相对便宜。它不复制 Goal_0或其任何子项。
另一个是 copy_term(Term, Copy, G_0s)可用于通过调用 maplist(call, G_0s) 重建附加的约束(在 SWI，Scryer 中)或 call(G_0) (在 SICStus)。在 SWI (clpfd) 和 Scryer (clpz) 的实现中， V in inf..sup 形式的一些冗余约束被投影省略。但投影确实是另一个问题。