Clarification about compound terms in the standard order of terms

Help!
1

Hi everyone,

I’m trying to understand how compound terms are ordered according to the standard order of terms. I know from the documentation that “Compound terms are first checked on their arity, then on their functor name (alphabetically) and finally recursively on their arguments, leftmost argument first.”.

But- what happens when a unit clause is compared to a non-unit clause (a fact to a rule) and both have the same functor and arity? I can’t seem to figure out the pattern in that. For instance, see the following examples:

?- _Ps = [p(a),p(b),p(A):-q(A)], sort(_Ps,Ss).          [1]
Ss = [p(a), p(b),  (p(A):-q(A))].

?- _Ps = [p(a),p(b),p(A,B):-q(A,B)], sort(_Ps,Ss).      [2]
Ss = [p(a), p(b),  (p(A, B):-q(A, B))].

?- _Ps = [p(a,b),p(b,c),p(A,B):-q(A,B)], sort(_Ps,Ss).  [3]
Ss = [(p(A, B):-q(A, B)), p(a, b), p(b, c)].

Above, all terms have the same (head) functor, p. In [1] the two unit clauses and one non-unit clause all have the same arity and the unit clauses are sorted as lower order. In [2] the non-unit clause has a higher arity and the unit clauses are still sorted as lower order. In [3] all the clauses have the same arity again but now the non-unit clause is sorted as lower order.

Is this something to do with the order of variables vs. atoms?

Is there a reliable way to know how a unit clause will be ordered relative to a non-unit clause in the standard order of terms?

2

@stassa.p Going by the rules at Standard Order of Terms, I’m also a bit befudled about how (p(A) :- q(A)) would be handled. Playing around with @<, I got the following:

?- (p(A) :- q(A)) @< p(a).
false.

?- (p(A) :- q(A)) @< p(a, b).
true.

I suspect (p(A) :- q(A)) may be converted into a compound term with something like clause (:Head, ?Body), but not sure what it would be seen as.

3

The principal functor of a term H :- B is (:-)/2 no matter what H and B are. That and the fact that :- is alphabetically before p explain all your examples.

4

@michaelby and @stassa.p, yup, just treating :- as any old functor solves the mystery:

?- :-(p(A),q(A)) @< p(a).
false.

?- :-(p(A),q(A)) @< p(a,b).
true.
5

Ah, oops. You’re right of course. :- is the functor, not p. Thanks for pointing it out.