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

实际上，它并没有真正成功。它乐观地成功（因为为了不停止计算，它必须成功）但实际的逻辑成功取决于剩余目标的实际成功。

如何以编程方式确定子目标是否成功实现剩余目标？（那我该怎么办？）方法是什么？

P.S.

具有次要 Prolog 真值可能是一个很好的 Prolog 扩展，因为 true+ 将指示 “在剩余目标成功的情况下成功”。这实际上似乎是有必要的：

在 SWI-Prolog 中，采用这个本质上模棱两可的目标：

do :- not_occupied(_).

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

?- do.
true.

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

Answer 1

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

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

第三种状态出现在顶层，此时列出了剩余目标。并且如何查询剩余目标取决于实现。典型的谓词是：

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 中它 returns 一对列表，也显示主要变量。另一方面，ECLiPSe Prolog 只有 returns 个虚拟变量。然后 call_residue_vars/2 存在兼容性问题，例如 here.

Answer 2

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

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

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

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

同样，这是一个答案替换，但这次它描述了无限多的解决方案。

答案和解决方案的概念通常可以互换使用，但是一旦我们使用延迟目标或约束，我们就需要明确区分。现在的新变化是答案可能包含任意数量的解决方案，包括 none。

?- 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 ?

residuum现在应该是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 的一些冗余约束。但是投影真的是另一个问题。

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

What is the approach for dealing with "residual goals" in Prolog?

prolog

prolog-coroutining