时间戳

首页 > 解决方案 > Prolog中处理“剩余目标”的方法是什么？

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

问题描述

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

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 扩展，因为 atrue+表示“在剩余目标成功的条件下成功”。这实际上似乎是有必要的：

在 SWI-Prolog 中，采用这个固有的模棱两可的目标：

do :- not_occupied(_).

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

?- do.
true.

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

标签： prologprolog-coroutining

解决方案

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

?- 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)统一。请注意，当某些约束变量存在于. 但主要的一点是，这个内置的实现起来相对便宜。它不复制或其任何子项。VarsGoal_0Goal_0Goal_0Goal_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投影省略了形式的一些冗余约束。但投影确实是另一个问题。

推荐阅读