Comparison and unification of arbitrary terms. Terms are ordered in the so-called “standard order''. This order is defined as follows:
-inf
. If the comparison
is equal, the float is considered the smaller value. If the Prolog flag
iso is defined, all
floating point numbers precede all rationals.
Although variables are ordered, there are some unexpected properties
one should keep in mind when relying on variable ordering. This applies
to the predicates below as to predicate such as sort/2
as well as libraries that reply on ordering such as library library(assoc)
and library
library(ordsets)
. Obviously, an established relation A
B
no longer holds if A is unified with e.g., a number. Also
unifying A with B invalidates the relation because
they become equivalent (==/2) after unification.
@<
As stated above, variables are sorted by address, which implies that they are sorted by‘age', where‘older' variables are ordered before‘newer' variables. If two variables are unified their‘shared' age is the age of oldest variable. This implies we can examine a list of sorted variables with‘newer' (fresh) variables without invalidating the order. Attaching an attribute, see section 8.1, turns an‘old' variable into a‘new' one as illustrated below. Note that the first always succeeds as the first argument of a term is always the oldest. This only applies for the first attribute, i.e., further manipulation of the attribute list does not change the‘age'.
?- T = f(A,B), A @< B. T = f(A, B). ?- T = f(A,B), put_attr(A, name, value), A @< B. false.
The above implies you can use e.g., an assoc (from library
library(assoc)
, implemented as an AVL tree) to maintain
information about a set of variables. You must be careful about what you
do with the attributes though. In many cases it is more robust to use
attributes to register information about variables.
Note that the standard order is not well defined on rational trees, also known as cyclic terms. This issue was identified by Mats Carlsson, quoted below. See also issue#1162 on GitHub.
Consider the terms A and B defined by the equations[1] A = s(B,0). [2] B = s(A,1).
- Clearly, A and B are not identical, so either
A @< B
orA @> B
must hold.
- Assume
A @< B
. But then,s(A,1) @> s(B,0)
i.e.,B @< A
. Contradicton.
- Assume
A @> B
. But then,s(A,1) @< s(B,0)
i.e.,B @< A
. Contradicton.
\+
Term1 == Term2
.<
, >
or =
, with the obvious meaning.