Prolog中的存在量词修饰符，使用setof/bagof

Question

我有一个关于在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).

有什么想法吗？在什么情况下需要使用unifier呢？

谢谢！

- oneAday

---

参见：什么是Prolog运算符“^”（“caret”）？，在那里我做了一个长注释来测试^的行为，但我对结果不满意。 - David Tonhofer

Answer 1

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

这与您在查询二元关系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

- ThomasH

---

谢谢 - 这很有帮助，但让我困惑的是^的实际用途。似乎每当需要统一特定变量时，只需将其包含在结果模板中（即在我们的情况下，将其从X更改为X-Z）-那么何时需要使用^运算符，而不将其包含在模板中呢？ - oneAday

@oneAday 嗯，我不知道我在答案中包含的查询结果是否澄清了事情。简单的答案是：使用 ^ 基本上表示“忽略此变量”。在模板中使用它表示“我对它感兴趣”，并将其作为结果集的一部分。这完全取决于您是否感兴趣。如果您不感兴趣，那么像“a-c”这样的结果会迫使您分解该术语，以便到达“c”。 - ThomasH

好的，我想我明白了 - 谢谢。我猜重点是，你希望/需要它被实例化，但不需要输出。 非常感谢你的帮助。 - oneAday

实际上，使用^将在回溯时忽略X的备选绑定，而__setof(Z, foo(_,Y,Z), C)__，这是另一种表达方式，表示您对第一个参数不感兴趣，仍将在回溯时考虑其备选值，并且您将获得3个可能的结果C-试试看。 - ThomasH