4.13.2.1 Existential Quantifier

X ^ P is recognized as meaning “there exists an X such that P is true”, and is treated as equivalent to simply calling P. The use of the explicit existential quantifier outside setof/3 and bagof/3 is superfluous.

Variables occurring in Generator will not be treated as free if they are explicitly bound within Generator by an existential quantifier. An existential quantification is written:

     Y^Q

meaning “there exists a Y such that Q is true”, where Y is some Prolog variable. For example:

     | ?- setof(X, Y^likes(X,Y), S).

would produce the single result

     X = _400,
     Y = _415,
     S = [bill,dick,harry,jan,tom] ;
     
     no

in contrast to the earlier example.

Furthermore, it is possible to existentially quantify a term, where all the variables in that term are taken to be existentially quantified in the goal. e.g.

     A=term(X,Y), setof(Z, A^foo(X,Y,Z), L).

will treat X and Y as if they are existentially quantified.


Send feedback on this subject.