Prolog：存在量化

Question

我想了解存在量化的用法。我现在所知道的是这种技术与 setof、findall、bagof 一起使用。此外，我发现了一个tutorial。但是，我不确定我何时以及如何在 Prolog 中进行 Vars^Goal（存在量化）。

举个例子，我的目标是找到两个相互认识但在不同公司工作的员工，将结果与L绑定，显示Name1-Name2:

company('Babbling Books', 500, 10000000).
company('Crafty Crafts', 5, 250000).
company('Hatties Hats', 25, 10000).

employee(mary, 'Babbling Books').
employee(julie, 'Babbling Books').
employee(michelle, 'Hatties Hats').
employee(mary, 'Hatties Hats').
employee(javier, 'Crafty Crafts').

knows(javier, michelle).

我的第一直觉是使用查询

?-employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2).

查询找到了答案，但没有将其呈现为正确的格式。正确的是：

?-setof(N1-N2, (C1,C2)^(employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2)), L).

我怎么理解(C1,C2)^(employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2))？它的概念是什么？谢谢。

Answer 1

I am not sure when and how I do the Vars^Goal (existentially quantifying) in Prolog.

最简单的答案是：永远不要这样做。您始终可以引入一个辅助谓词，它准确地捕获您想要的查询，准确地公开您想要的参数而不是其他任何东西（这需要量化），并且有一个很好的自记录名称。

在你的例子中，你可以定义：

different_company_acquaintances(N1, N2) :-
    employee(N1, C1),
    employee(N2, C2),
    C1 \= C2,
    knows(N1, N2).

然后将您的 setof 查询表达为：

?- setof(N1-N2, different_company_acquaintances(N1, N2), L).
L = [javier-michelle].

由于谓词名称以及它隐藏了不相关的实现细节，因此更易于阅读。请注意，在谓词定义中，参数仅是调用者关心的数据（员工），而没有调用者不关心的数据（公司）的参数。

How could I understand the (C1,C2)^(employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2)) ?

^ 语法，无论确切的正确形式是什么，都是为了表明变量，如果您写出单独的谓词定义，则只会出现在谓词的主体中，而不是作为其参数。这告诉 setof 和朋友，每次它尝试执行目标 (employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2)) 时，它应该使用未绑定的变量 C1 和 C2。换句话说，它不应该试图从一次尝试到下一次尝试保留 C1 和 C2 的值。

Prolog：存在量化

Prolog: existentially quantifying

prolog

existential-operator

prolog-setof