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

提问于 2024-04-25T10:28:11+08:00

浏览次

4

我有一个快速的问题 . 在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).

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

谢谢！

1 回答

2
好吧，我不确定我能否完美地解释它，但让我试一试 .

它与你在查询2-ary关系 mother/2 这一事实有关 . 在 that 情况下，使用 X-S 作为模板对结果集 C 具有类似的效果，就像在目标前面使用 S^ 一样 . 在 X-S 中，您在模板中使用了两个变量，因此X和S的每个可能绑定都包含在C中 . 您在目标前使用 S^ 获得相同的效果，因为这是在说"ignore bindings of S when constructing the result" .

但是，当您查询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 有效地改变了你的结果集 .

希望有所帮助 .

Edit ：当我包含上述两个查询的结果时，它可能会澄清事情 . 第一个是这样的：
```
?- 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
```
回复于 2024-04-25T10:28:11+08:00

相关问题