带有 ^ 标记的 Prolog 理解 setof/3 [英] Prolog understanding setof/3 with ^ markings

问题描述

有人可以向我解释一下这是做什么的吗?

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

我已经阅读了setof的文档；我的理解是第三个论点与事实相统一.

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

完整的片段是:

<预><代码>solve_task_bt(go(Target),Agenda,ClosedSet,F,G,NewPos,RR,BackPath) :-议程 = [当前|休息]，电流 = [c(F,G,P)|RPath],新议程=休息，袋 = 搜索(P，P1，R，C)，(\+ setof((P1,C),P^R^Bag,PS) -> solve_task_bt(go(Target),Rest,[Current|ClosedSet],F,G,NewPos,RR,BackPath);否则 ->setof((P1,C),P^R^Bag,PS),addChildren(PS,RPath,Current,NewAgenda,Target,Result),NewClosedSet = [Current|ClosedSet],最新议程 = 结果，solve_task_bt(go(Target),NewestAgenda,NewClosedSet,F1,G1,Pos,P|RPath,BackPath)).% 回溯搜索

解决方案

稍后更新:以下不太正确，最好转到父参考:什么是 Prolog 运算符 ^?

所以，只关注setof/3

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

让我们将 Bag 替换为它的语法等价物，并在前一行设置:

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).搜索(2，a，m，g).搜索(2，a，m，j).搜索(1，a，m，j).搜索(3，a，w，j).搜索(3，a，v，j).搜索(2，b，v，g).搜索(3，b，m，g).搜索(5，b，m，g).搜索(1，b，m，j).搜索(1，b，v，j).搜索(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).

没有关于单一变量"的编译器警告，而

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

会给你投诉:

单变量:[P,R]

这是有原因的:P 和 R 在子句级别"可见.这里我们将 P 和 R 添加到头部，这给我们以后的打印输出很好.

封闭解决方案

我们能做的:

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

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

搜索(P,X,P,Y)

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

由于 (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 处理器的查询是:

<块引用>

构造Bag，它是一个[X,Y]的列表，使得:

∀ [X,Y]: ∃P,∃R: search(P,X,R,Y) 是真的.

开放解决方案

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

在这种情况下，Bag 包含 fixed (P,R) 的所有解决方案 元组，Prolog 允许您在 setof 级别回溯可能的 (P,R)/3 谓词.变量 P 和 R 在 setof/3 之外可见".

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

<块引用>

构造 P,R 使得:

你可以构造Bag，它是一个[X,Y]的列表，使得

∀ [X,Y]: search(P,X,R,Y) 为真.

符号问题

如果 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) :- 搜索(_,X,_,Y).

这也将说明发生了什么，因为变量不会在它们出现的子句之外导出.

Could someone explain to me what this is doing?

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

I have read the documentation of setof; my understanding is that the thrid argument gets unified with the facts.

However, I can't make sense of the code snippet above.

The full snippet is:

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

解决方案

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

So, just focusing on the setof/3

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

Let's replace Bag by its syntactic equivalent set a line earlier:

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

The description of setof/3 says that it

• Calls argument 2 as a goal;
• Collects the solutions according to argument 1, the template;
• Puts the result of the templating into argument 3, the bag, leaving out duplicates.

So in this case, setof/3 will call (give the expression to the Prolog processor to prove) search(P,P1,R,C), and when this succeeds, collect the resulting values P1,C as a conjunction (P1,C) (which is really special, why not use a 2-element list?) and put everything into PS

Let's just try a runnable example similar to the above, using a list instead of the conjunction and using different names:

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

Notice that you can write

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

without the compiler warning about "singleton variables", whereas

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

will give you a complaint:

Singleton variables: [P,R]

and there is a reason for that: P and R are visible at "clause level". Here we add P and R to the head, which gives us good printout later.

Closed solution

The we can do:

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

Bag now contains all possible solutions [X,Y] for:

search(P,X,P,Y)

where we don't care about the values of the (P,R) tuple outside of the inner goal. Values of P and R are invisible outside the goal called by setof/3, backtracking stays "internal".

Alternative solution for [X,Y] due to differing (P,R) are collapsed by setof/3. If one was using bagof/3 instead:

?- 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], ....

In effect, the query to the Prolog Processor is:

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

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

Open solution

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

In this case, Bag contains all solutions for a fixed (P,R) tuple, and Prolog allows you to backtrack over the possible (P,R) at the level of the setof/3 predicate. Variables P and R are "visible outside" of setof/3.

In effect, the query to the Prolog Processor is:

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.

A problem of notation

This would be clearer if Prolog had had a Lambda operator to indicate where the cross-level attach points (i.e. between metapredicate and predicate) are. Assuming what is in setof/3 stays in setof/3 (the opposite attitude of Prolog), one would be able to write:

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

or

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

and

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

Or one could simply write

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

search_closed(X,Y) :- search(_,X,_,Y).

which would also make clear what is going as variables are not exported outside of the clause they appear in.

这篇关于带有 ^ 标记的 Prolog 理解 setof/3的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！