5

我有一个快速的问题。在序言中使用 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).

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

谢谢！

4

1 回答 1

3

好的，我不确定我能否完美地解释它，但让我试试。

这与您查询 2 元关系的事实有关，mother/2. 在这种情况下，X-S作为模板使用对结果集的影响与在目标前面C使用类似。S^在X-S您使用模板中的两个变量时，因此 X 和 S 的每个可能绑定都包含在 C 中。您S^在目标前面使用会获得相同的效果，因为这表示“在构造结果时忽略 S 的绑定” .

但是当您查询三元关系时，两者之间的区别会变得更加清晰。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
于 2010-01-05T10:12:28.860 回答