prolog 中的存在限定符,使用 setof/bagof [英] existential qualifier in prolog, using setof / bagof
问题描述
我有一个简短的问题.在序言中使用 setof 的存在限定符(即 ^).
I had a quick question re. existential qualifier using setof in prolog (i.e. ^).
使用 SICStus 似乎(尽管许多网站声称),S 确实似乎在下面的代码中被量化(使用沼泽标准,事实之母/事实之子,我没有包括在这里):
using SICStus it seems that (despite what a number of websites claim), S does indeed appear to be quantified in the code below (using the bog standard, mother of / child of facts, which i havent included here):
child(M,F,C) :- setof(X,(mother(S,X)),C).
我使用以下方法检查统一:
i check the unification using:
child(M,F,C) :- setof(X-S,(mother(S,X)),C).
所以下面的代码,与存在运算符似乎没有区别:
so the following code, with the existential operator seem to make no difference:
child(M,F,C) :- setof(X,S^(mother(S,X)),C).
知道这是为什么吗?那么在什么情况下您需要统一器?
Any ideas why this is? What would be a situation where you would need the unifier then?
谢谢!
推荐答案
好吧,我不确定我能不能完美地解释它,但让我试试.
Ok, I'm not sure I can explain it perfectly, but let me try.
这与您正在查询二元关系 mother/2
的事实有关.在那种情况下,使用 XS
作为模板对结果集 C
的影响与使用 S^
在球门前.在 XS
中,您在模板中使用了两个变量,因此 X 和 S 的每个可能的绑定都包含在 C 中.使用 S^
在前面获得相同的效果目标,因为这是说在构造结果时忽略 S 的绑定".
It has to do with the fact that you are querying over a 2-ary relation, mother/2
. In that case using X-S
as the template has a similar effect on the result set C
as using S^
in front of the goal. In X-S
you are using both variables in the template, and therefore each possible binding of X and S is included in C. You get the same effect using S^
in front of the goal, as this is saying "ignore bindings of S when constructing the result".
但是当您查询三元关系时,两者之间的区别变得更加清晰.SWI手册有这个例子:
But the difference between the two becomes clearer when you query over a 3-ary relation. The SWI manual has this example:
foo(a, b, c).
foo(a, b, d).
foo(b, c, e).
foo(b, c, f).
foo(c, c, g).
现在执行与示例中类似的查询
Now do similar queries as in your example
setof(X-Z, foo(X,Y,Z), C).
和
setof(Z, X^foo(X,Y,Z), C).
你会得到不同的结果.
这不仅仅是检查统一性,X-Z
有效地改变了你的结果集.
It's not just checking unification, X-Z
effectively changes your result set.
希望有所帮助.
编辑:当我包含上面两个查询的结果时,也许它会澄清一些事情.第一个是这样的:
Edit: Maybe it clarifies things when I include the results of the two queries above. The first one goes like this:
?- 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
这篇关于prolog 中的存在限定符,使用 setof/bagof的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!