Prolog中处理“剩余目标”的方法是什么？

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}？事情可能变得相当复杂（阅读：越野车）。此外，撤消绑定是一项艰巨的任务。或实现首先创建整个目标的副本，然后保留约束。

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 形式的一些冗余约束。但投影确实是另一个问题。

Answer 2

无法解决其剩余目标的查询称为挣扎查询。当计算打算成功或有限失败时，它们可能会陷入困境。剩余目标引入了第三种状态，既不是成功也不是无限失败。

约束逻辑程序可能无法调用某些约束求解器，因为变量实例化或约束不足。为了避免在约束求解器中陷入困境，他们通常将标签作为最后的手段。

当列出剩余目标时，可以在顶层看到第三个状态。如何查询剩余目标取决于实现。典型的谓词是：

• call_residue_vars(G, L)：
  只要目标 G 成功并统一 L，谓词就成功 使用新引入的属性变量。
• call_residue(G, L)：
  只要目标 G 成功并统一 L，谓词就成功 使用新引入的属性变量的约束。

SWI-Prolog 不在顶层打印残差变量，是 SWI-Prolog 的一项服务，仅显示投影变量。但是你仍然可以查询残差：

/* SWI-Prolog */
?- do.
true.

?- call_residue_vars(do, X).
X = [_5968],
when(ground(_5968), \+location(_6000, _5968)).

遗憾的是 SWI-Prolog 不支持 call_residue/2。 copy_term/3 并不是真正的替代品。在我的 Prolog 系统中，我已经停止计算顶层的投影并显示一切。我也支持 call_residue/2：

/* Jekejeke Prolog */
?- do.
when(ground([_A]), \+ location(_B, _A))

?- call_residue_vars(do, X).
X = [_A],
when(ground([_A]), \+ location(_B, _A))

?- call_residue(do, X).
X = [when(ground([_A]), \+ location(_B, _A))],
when(ground([_A]), \+ location(_B, _A))

call_residue/2 也可以在 ECLiPSe Prolog 和 SICStus Prolog 中找到。在 SICStus Prolog 中，它返回一个配对列表，也显示主要变量。另一方面，ECLiPSe Prolog 仅返回虚拟变量。然后还有 call_residue_vars/2 的兼容性问题，比如here。