The existentially quantifying

Help! Tools
,
1

As a newbie in learning the Prolog, I got a question about how to properly use the existentially quantifying technique.

Here I have facts, 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).

which formats to L = [javier-michelle].

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. The same question is posted on StackOverflow, but people there recommend me to ask here.

1 Like
2

I must say that (C1,C2)^(...) is not the syntax I have always known.
Indeed I would write it like C1^C2^(...). Maybe they are the same.
Anyway, bagof/3 documentation attempts to explain the effect that an existentially qualified variable has in the aggregation process. It changes the GROUP BY list, just to draw a loose parallel with SQL.

2 Likes
3

They are the same. In the end it is interpreted as TermWithExistentialVars^Goal. It doesn’t matter what shape TermWithExistentialVars takes. e.g, C1^C2 or (C1,C2) or v(C1,C2) or [C1,C2], etc.

edit the system uses (a variant of) term_variables/2 on TermWithExistentialVars .

3 Likes