I am trying to understand the usage of existentially quantifying. What I know by now is this technique is used with setof, findall, bagof. Further, I found a tutorial. However, I am not sure when and how I do the Vars^Goal (existentially quantifying) in Prolog.
Here is the example, my goal is to find two employees who know each other but work at different companies, binding the result with L showing 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).
My first instinct is to use the query
?-employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2).
The query found the answer but doesn't render it into the correct format. The correct one is:
?-setof(N1-N2, (C1,C2)^(employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2)), L).
How could I understand the (C1,C2)^(employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2)) ? And what's the concept of it? Thanks.
I am not sure when and how I do the Vars^Goal (existentially quantifying) in Prolog.
The easiest answer is: Don't do it, ever. You can always introduce an auxiliary predicate that captures exactly the query you want, exposing exactly the arguments you want and nothing else (that would require quantification), and with a nice self-documenting name.
In your example, you can define:
different_company_acquaintances(N1, N2) :-
employee(N1, C1),
employee(N2, C2),
C1 \= C2,
knows(N1, N2).
and then express your setof query as:
?- setof(N1-N2, different_company_acquaintances(N1, N2), L).
L = [javier-michelle].
This is easier to read because of the predicate name and because it hides the irrelevant implementation details. Note that in the predicate definition the arguments are only the data the caller cares about (the employees), and there are no arguments for the data the caller doesn't care about (the companies).
How could I understand the
(C1,C2)^(employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2))?
The ^ syntax, whatever the exact correct form is, is meant to signal variables that, if you wrote out a separate predicate definition, would only occur in the predicate's body, not as its arguments. This tells setof and friends that every time it tries to execute the goal (employee(N1,C1),employee(N2,C2),C1\=C2,knows(N1,N2)) it should do so with unbound variables C1 and C2. In other words, it should not try to retain the values of C1 and C2 from one attempt to the next.