Prolog 理解 setof/3 带有 ^ 标记

Question

谁能给我解释一下这是做什么的？

(\+ setof((P1,C),P^R^Bag,PS) -> ...
otherwise ->...

我已经阅读了setof的文档；我的理解是，第三种说法与事实相统一。

但是，我无法理解上面的代码片段。

完整的片段是：


solve_task_bt(go(Target),Agenda,ClosedSet,F,G,NewPos,RR,BackPath) :-
  Agenda = [Current|Rest],
  Current = [c(F,G,P)|RPath],
  NewAgenda = Rest,
  Bag = search(P,P1,R,C),
  (\+ setof((P1,C),P^R^Bag,PS) -> solve_task_bt(go(Target),Rest,[Current|ClosedSet],F,G,NewPos,RR,BackPath);
    otherwise -> 
    setof((P1,C),P^R^Bag,PS),
    addChildren(PS,RPath,Current,NewAgenda,Target,Result),
    NewClosedSet = [Current|ClosedSet],
    NewestAgenda = Result,
    solve_task_bt(go(Target),NewestAgenda,NewClosedSet,F1,G1,Pos,P|RPath,BackPath)
    ).  % backtrack search

Answer 1

Update a bit later: The below is not quite correct, better go to the parent reference: What is the Prolog operator ^?

所以，只关注 setof/3

setof((P1,C),P^R^Bag,PS)

让我们将 Bag 替换为它的句法等价物 set a line earlier:

setof((P1,C),P^R^search(P,P1,R,C),PS)

setof/3 的描述说

调用参数 2 作为目标;
根据参数1收集解决方案，模板;
将模板化的结果放入参数 3，bag，省略重复项。

所以在这种情况下，setof/3将调用（将表达式交给Prolog处理器证明）search(P,P1,R,C)，当调用成功时，收集结果值P1，C 作为 conjunction (P1,C)（这真的很特别，为什么不使用 2 元素列表？）并将所有内容放入 PS

让我们尝试一个类似于上面的可运行示例，使用列表而不是连词并使用不同的名称：

search(1,a,n,g).
search(2,a,m,g).

search(2,a,m,j).
search(1,a,m,j).
search(3,a,w,j).
search(3,a,v,j).

search(2,b,v,g).
search(3,b,m,g).
search(5,b,m,g).

search(1,b,m,j).
search(1,b,v,j).

search(2,b,w,h).

get_closed(Bag)   :- setof([X,Y],P^R^search(P,X,R,Y),Bag). 
get_open(Bag,P,R) :- setof([X,Y],    search(P,X,R,Y),Bag).

注意你可以写

get_closed(Bag) :- setof([X,Y],P^R^search(P,X,R,Y),Bag).

没有关于 "singleton variables" 的编译器警告，而

get_open(Bag) :- setof([X,Y],search(P,X,R,Y),Bag).

会给你投诉：

Singleton variables: [P,R]

这是有原因的：P 和 R 在 "clause level" 处可见。这里我们将 P 和 R 添加到头部，这给了我们稍后良好的打印输出。

封闭解

我们能做的：

?- get_closed(Bag).
Bag = [[a, g], [a, j], [b, g], [b, h], [b, j]].

Bag 现在包含所有可能的解决方案 [X,Y]：

search(P,X,P,Y)

我们不关心内部目标之外的 (P,R) 元组的值。 P 和 R 的值在 setof/3 调用的目标之外是不可见的，回溯停留在 "internal".

由于 (P,R) 不同，[X,Y] 的替代解决方案被 setof/3 折叠。如果有人使用 bagof/3 代替：

?- bagof([X,Y],P^R^search(P,X,R,Y),Bag).
Bag = [[a, g], [a, g], [a, j], [a, j], [a, j], [a, j], [b, g], ....

实际上，对 Prolog 处理器的查询是：

Construct Bag, which is a list of [X,Y] such that:

∀ [X,Y]: ∃P,∃R: search(P,X,R,Y) is true.

打开解决方案

?- get_open(Bag,P,R).
Bag = [[a, j], [b, j]],
P = 1,
R = m ;
Bag = [[a, g]],
P = 1,
R = n ;
Bag = [[b, j]],
P = 1,
R = v ;
Bag = [[a, g], [a, j]],
P = 2,
R = m ;
Bag = [[b, g]],
P = 2,
R = v ;
Bag = [[b, h]],
P = 2,
R = w ;
Bag = [[b, g]],
P = 3,
R = m ;
Bag = [[a, j]],
P = 3,
R = v ;
Bag = [[a, j]],
P = 3,
R = w ;
Bag = [[b, g]],
P = 5,
R = m.

在这种情况下，Bag 包含固定 (P,R)[= 的所有解决方案136=] 元组，Prolog 允许您在 setof/3 谓词级别回溯可能的 (P,R)。变量 P 和 R 是 setof/3 的 "visible outside"。

实际上，对 Prolog 处理器的查询是：

Construct P,R such that:

you can construct Bag, which is a list of [X,Y] such that

∀ [X,Y]: search(P,X,R,Y) is true.

符号问题

如果 Prolog 有一个 Lambda 运算符来指示跨级附加点（即元谓词和谓词之间）的位置，这会更清楚。假设 setof/3 中的内容保留在 setof/3 中（Prolog 的相反态度），可以这样写：

get_closed(Bag) :- setof([X,Y],λX.λY.search(P,X,R,Y),Bag).

或

get_closed(Bag) :- setof([X,Y],search(P,X,R,Y),Bag).

和

get_open(Bag) :- λP.λR.setof([X,Y],search(P,X,R,Y),Bag).

或者可以简单地写

get_closed(Bag) :- setof([X,Y],search_closed(X,Y),Bag). search_closed(X,Y) :- search(_,X,_,Y).

这也可以弄清楚发生了什么，因为变量不会导出到它们出现的子句之外。

Prolog 理解 setof/3 带有 ^ 标记

Prolog understanding setof/3 with ^ markings

prolog

prolog-setof

封闭解

打开解决方案

符号问题

或者可以简单地写