What is the Prolog operator ^ ?
Looking at The Prolog Built-in Directive op gives a list of the built-in operators.
I see
** is exponentiation/\ is orbut what is ^ ?
Each of the three current answers are of value and I learned something:
The operator (^)/2 serves several purposes:
setof/3, bagof/3Here it is used to denote the existential variables (set) of a term. Like in
setof(Ch, P^child_of(Ch,P), Chs) where P is declared as an existential variable.
As a non-standard side effect to this, many systems have defined it as predicate with the following definition:
_^Goal :- Goal
But then, others do not have such a definition. It is in any case a good idea to avoid to define a predicate (^)/2.
(^)/2 - powerThis is an evaluable functor accessible via (is)/2 and arithmetic comparison like (=:=)/2 and (>)/2. Also library(clpfd) uses it with this meaning. In contrast to (**)/2 which always results in a float, 2^2 is an integer - thereby permitting arithmetics with bigints. Just try ?- X is 7^7^7. to see if your system supports them.
Finally, there are user defined uses for (^)/2 that do not collide with above uses like lambda expressions via library(lambda) (source).
There are a few general remarks about its use. (^)/2 associates to the right which means that:
(7^7^7) = (7^(7^7)). It has a very low priority which means that you have to use brackets for arguments with standard operators.
In math expressions, ^ is exponentiation, it's just different notation for **.
In lambda expressions, it is a parameter-passing operator.
As in Pereira and Shieber's book:
Thus the lambda expression λ x. x + 1 would be encoded in Prolog as X^(X+1). Similarly, the lambda expression λ x. λ y.wrote(y, x) would be encoded as the Prolog term X^Y^wrote(Y,X), assuming right associativity of "^"
In Prolog, most symbols can be used 'uninterpreted', at syntactic level, in particular after an op/3 declaration, any atom can be used as operator. Then you can use, for instance, ^/2 as a function constructor for a domain specific language (a DSL), with a semantic specified from your rules.
Is SWI-Prolog (or more generally in ISO Prolog), current_op/3 gives you information about declared operators:
?- current_op(X,Y,^).
X = 200,
Y = xfy.
That said, any Prolog implementing setof/3 is expected to interpret ^/2 as a quantification specifier, when put to decorate the 2nd argument. As well, any Prolog implementing is/2 is expected to interpret ^/2 as exponentiation, when occurring on the right side of the is/2 expression.
Here's my addition to the use of ^ in setof/3 and bagof/3.
Upfront note:
Personally, I consider the semantics of ^ to be a failure, because it looks as if this were an "existential quantification" and is even described as such sometimes (for example: GNU Prolog, SWI-Prolog library(yall)) but it actually is NOT. Avoid this misfeature, write a separate predicate to be called by setof/3 and bagof/3 instead. An ISO Prolog-2, if it ever happens, should really clean this up.
We start with an overview ASCII Image:
Clause-wide variable
|
|
+------------------------+------------------------+
| |
| Clause-wide variables |
| that are collected via the |
| template at arg-position 1 by |
| setof/3 (NOT local to setof/3) |
| thus can be constrained elsewhere |
| in the clause (possibly accidentally) |
| | |
| | |
| +-+--------+----------+-+ |
| | | | | |
| | | | | |
get_closed_set(Set,K) :- setof( [X,Y] , P^R^search(P,R,X,Y,K) , Set).
| | | | | |
| <-------------------> Goal expression
| | | | | |
| | | | | |
+---------------------------------------+-----+
| | | | |
| | | | |
+-+----+---+-+ Clause-wide variable.
| Backtracking over this
| is done by the caller
| of get_closed_set/2.
|
Variables marked as "free for
backtracking if fresh".
This is NEARLY the same as "being
local to the goal expression" or
"being existentially quantified."
Backtracking over these is done by setof/3.
If these appear elsewhere in the clause,
they be constrained (possibly accidentally)!
search(1,n,a,g).
search(2,m,a,g).
search(2,m,a,j).
search(1,m,a,j).
search(3,w,a,j).
search(3,v,a,j).
search(2,v,b,g).
search(3,m,b,g).
search(5,m,b,g).
search(2,w,b,h).
% ===
% HATTY EXPRESSIONS ("CLOSED EXPRESSIONS")
% ===
% If P and R do not appear anywhere else than in the goal expression.
% "P^R^" (not quite) closes off variables P,R: they are not (not quite)
% invisible outside of the goal expression "P^R^search(P,R,X,Y)"
get_closed_set(Set) :- setof( [X,Y] , P^R^search(P,R,X,Y) , Set).
get_closed_bag(Bag) :- bagof( [X,Y] , P^R^search(P,R,X,Y) , Bag).
% The above is the same as this (which I recommend for clarity and
% to avoid annoying bug searches):
indirect_search(X,Y) :- search(_P,_R,X,Y).
get_closed_set_indirect(Set) :- setof( [X,Y] , indirect_search(X,Y) , Set).
get_closed_bag_indirect(Bag) :- bagof( [X,Y] , indirect_search(X,Y) , Bag).
% ===
% NONHATTY EXPRESSIONS ("OPEN EXPRESSIONS")
% ===
get_open_set(Set,P,R) :- setof( [X,Y] , search(P,R,X,Y) , Set).
get_open_bag(Bag,P,R) :- bagof( [X,Y] , search(P,R,X,Y) , Bag).
% ===
% TESTING
% ===
:- begin_tests(hat_operator).
test(clo_set) :- get_closed_set(Set),
format("Closed Set:\n ~q\n",[Set]),
Set = [[a,g],[a,j],[b,g],[b,h]].
test(clo_bag) :- get_closed_bag(Bag),
format("Closed Bag:\n ~q\n",[Bag]),
Bag = [[a,g],[a,g],[a,j],[a,j],[a,j],[a,j],[b,g],[b,g],[b,g],[b,h]].
test(clo_set_ind) :- get_closed_set_indirect(Set),
format("Closed Set, indirect:\n ~q\n",[Set]),
Set = [[a,g],[a,j],[b,g],[b,h]].
test(clo_bag_ind) :- get_closed_bag_indirect(Bag),
format("Closed Bag, indirect:\n ~q\n",[Bag]),
Bag = [[a,g],[a,g],[a,j],[a,j],[a,j],[a,j],[b,g],[b,g],[b,g],[b,h]].
test(opn_set) :- bagof(solution(Set,P,R), get_open_set(Set,P,R), OuterBag),
format("Bag for get_open_set/3:\n ~q\n",[OuterBag]).
test(opn_bag) :- bagof(solution(Bag,P,R), get_open_bag(Bag,P,R), OuterBag),
format("Bag for get_open_bag/3:\n ~q\n",[OuterBag]).
:- end_tests(hat_operator).
rt :- run_tests(hat_operator).
When we run rt, nothing unexpected occurs, we are like Fonzi with existential quantifiers:
Closed Set: [[a,g],[a,j],[b,g],[b,h]]
Closed Bag: [[a,g],[a,g],[a,j],[a,j],[a,j],[a,j],
[b,g],[b,g],[b,g],[b,h]]
Closed Set, indirect: [[a,g],[a,j],[b,g],[b,h]]
Closed Bag, indirect: [[a,g],[a,g],[a,j],[a,j],[a,j],[a,j],
[b,g],[b,g],[b,g],[b,h]]
Bag for get_open_set/3: [solution([[a,j]],1,m),solution([[a,g]],1,n),
solution([[a,g],[a,j]],2,m),solution([[b,g]],2,v),
solution([[b,h]],2,w),solution([[b,g]],3,m),
solution([[a,j]],3,v),solution([[a,j]],3,w),
solution([[b,g]],5,m)]
Bag for get_open_bag/3: [solution([[a,j]],1,m),solution([[a,g]],1,n),
solution([[a,g],[a,j]],2,m),solution([[b,g]],2,v),
solution([[b,h]],2,w),solution([[b,g]],3,m),
solution([[a,j]],3,v),solution([[a,j]],3,w),
solution([[b,g]],5,m)]
You may have to run this to see more list output (case of SWI-Prolog):
set_prolog_flag(answer_write_options,[max_depth(100)]).
set_prolog_flag(debugger_write_options,[max_depth(100)]).
If you enter the following, Prolog correctly warns about "singleton variables P,R". Good.
get_open_set(Set) :- setof([X,Y],search(P,R,X,Y),Set).
This is accepted and could be given a meaning, but Prolog will be looking for procedure ^/2 on call and say that "^/2 can only appear as the 2nd argument of setof/3 and bagof/3". Okay.
get_outerly_closed_set(Set) :- P^R^setof([X,Y],search(P,R,X,Y),Set).
A possible meaning for the above might be the utterly mundane:
get_outerly_closed_set(Set) :- close_it_off(Set).
close_it_off(Set) :- setof([X,Y],search(_P,X,_R,Y),Set).
Now we are getting into "failure of semantics" territory: Prolog does not consider the outside P as a variable different from the P in P^. This is why P^ does NOT mean "∃P such that":
get_closed_set_weird_1(Set,P) :-
setof( [X,Y] , P^R^search(P,R,X,Y) , Set),
format("P=~q\n",[P]).
?- get_closed_set_weird_1(Set,P).
P=_14996
Set = [[a, g], [a, j], [b, g], [b, h]].
?- get_closed_set_weird_1(Set,1).
P=1
Set = [[a, g], [a, j]].
No warnings occur if you write such a thing:
get_closed_set_weird_2(Set) :-
setof( [X,Y,P], P^R^search(P,R,X,Y), Set).
?- get_closed_set_weird_2(Set).
Set = [[a, g, 1], [a, g, 2], [a, j, 1], [a, j, 2], [a, j, 3], ...
In fact, P^ ends up being ignored. The above is the same as:
get_closed_set_weird_2e(Set) :-
setof( [X,Y,P], R^search(P,R,X,Y), Set).
This is entirely expected behaviour, but a casual reading of setof([X,Y], ... would lead one to think that [X,Y] are free variables over which setof/3 ranges. This is not the case: [X,Y] is just a template and X and Y are actually clause-wide variables, which can be constrained elsewhere:
get_closed_set_weird_2(Set,X) :-
setof( [X,Y], P^R^search(P,R,X,Y) , Set),
format("X=~q\n",[X]).
?- get_closed_set_weird_2(Set,X).
X=_20346
Set = [[a, g], [a, j], [b, g], [b, h]].
?- get_closed_set_weird_2(Set,b).
X=b
Set = [[b, g], [b, h]].
The above would have been more clear as
get_closed_set_weird_2c(Set,V) :-
setof( [V,Y], close_it_off(V,Y), Set),
format("V=~q\n",[V]).
close_it_off(X,Y) :- search(_P,_R,X,Y).
?- get_closed_set_weird_2c(Set,V).
V=_21682
Set = [[a, g], [a, j], [b, g], [b, h]].
but note that this is absolutely not the same as this, where we backtrack over V outside of setof/3:
get_closed_set_weird_2x(Set,V) :-
setof( [X,Y], close_it_off(V,X,Y), Set),
format("V=~q\n",[V]).
close_it_off(V,X,Y) :- V=X,search(_P,_R,X,Y).
?- get_closed_set_weird_2x(Set,V).
V=a
Set = [[a, g], [a, j]], V = a ;
V=b
Set = [[b, g], [b, h]], V = b.
One would like to have a clean way of indicating which variables of the goal expression are visible outside of the goal expression, which ones are not, and which ones to range over.
How about this:
λX. at the head of the goal expression, the X is visible outside the goal expression. Any X elsewhere in the clause is the same X.∃X. at the head of the goal expression, the X is invisible outside the goal expression. Any X elsewhere in the clause is a different X (you are then invited to proceed to rename by the editor).X that appears in the goal expression without a preceding λX. or a ∃X. is a compiler error. λX. and any variables appearing as ∃X. (Don't complain about the lowercase x above; it just looks that way. λX. ∃X. Xx)