prolog - prolog 中的存在限定符，使用 setof/bagof

Question

我有一个简短的问题。在序言中使用 setof 的存在限定符(即 ^)。

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

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

有什么想法吗？那么什么情况下您需要统一器？

谢谢!

Answer 1

好吧，我不确定我能否完美地解释它，但让我尝试一下。

这与您正在查询二元关系 mother/2 的事实有关。在这种情况下，使用 X-S 作为模板对结果集 C 的效果与使用 S^ 的效果类似球门前面。在 X-S 中，您在模板中使用了这两个变量，因此 X 和 S 的每个可能的绑定(bind)都包含在 C 中。在前面使用 S^ 可以获得相同的效果目标，因为这意味着“构建结果时忽略 S 的绑定(bind)”。

但是当您查询三元关系时，两者之间的区别会变得更加清晰。 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