prolog中的存在性限定符,使用setof / bagof

2023年9月7日 339次阅读

我有一个快速的问题.在prolog中使用setof的存在性限定符(即^).

使用SICStus似乎(尽管许多网站声称),S确实似乎在下面的代码中量化(使用沼泽标准,事实的母亲/事实的孩子,我没有包括在这里)：

child(M,F,C) :- setof(X,(mother(S,X)),C).

我使用以下方法检查统一：

child(M,F,C) :- setof(X-S,(mother(S,X)),C).

所以下面的代码,与存在运算符似乎没有区别：

child(M,F,C) :- setof(X,S^(mother(S,X)),C).

任何想法为什么会这样？那么你需要统一者的情况是什么？

谢谢！

最佳答案 好吧,我不确定我能否完美地解释它,但让我试试吧.

它与你正在查询2-ary关系,母亲/ 2这一事实有关.在这种情况下,使用X-S作为模板对结果集C具有与在目标前面使用S ^类似的效果.在XS中,您在模板中使用了两个变量,因此X和S的每个可能的绑定都包含在C中.您可以在目标前使用S ^获得相同的效果,因为这是“在构造时忽略S的绑定”结果”.

但是,当您查询3-ary关系时,两者之间的差异会变得更加清晰. SWI手册有这个例子：

foo(a, b, c).
foo(a, b, d).
foo(b, c, e).
foo(b, c, f).
foo(c, c, g).

现在执行与示例中类似的查询

setof(X-Z, foo(X,Y,Z), C).

和

setof(Z, X^foo(X,Y,Z), C).

你会得到不同的结果.

它不只是检查统一,X-Z有效地改变了你的结果集.

希望有所帮助.

编辑：当我包含上述两个查询的结果时,它可能会澄清事情.第一个是这样的：

?- setof(X-Z, foo(X,Y,Z), C).   
Y = b
C = [a-c, a-d] ;
Y = c
C = [b-e, b-f, c-g] ;
No

第二个产生：

?- setof(Z, X^foo(X,Y,Z), C).
Y = b
C = [c, d] ;
Y = c
C = [e, f, g] ;
No
点赞