The ordering relation on terms used by ACL2
ACL2 must occasionally choose which of two terms is syntactically smaller. The need for such a choice arises, for example, when using equality hypotheses in conjectures (the smaller term is substituted for the larger elsewhere in the formula), in stopping loops in permutative rewrite rules (see loop-stopper), and in choosing the order in which to try to cancel the addends in linear arithmetic inequalities. When this notion of syntactic size is needed, ACL2 uses ``term order.'' Popularly speaking, term order is just a lexicographic ordering on terms. But the situation is actually more complicated.
We define term order only with respect to terms in translated form. See trans. Constants are viewed as built up by pseudo-function applications, as described at the end of this documentation.
(a) the number of variable occurrences in
term1is less than that in term2, or
(b) the numbers of variable occurrences in the two terms are equal but the number of function applications in
term1is less than that in term2, or
(c) the numbers of variable occurrences in the two terms are equal, the numbers of functions applications in the two terms are equal, but pseudo-function application count for
term1is less than that for term2, or
(d) the numbers of variable occurrences in the two terms are equal, the numbers of functions applications in the two terms are equal, the pseudo-function application counts for the two terms are equal, and
term1comes before term2in a lexicographic ordering, lexorder, based their structure as Lisp objects: see lexorder.
By ``number of variable occurrences'' we do not mean ``number of distinct
variables'' but ``number of times a variable symbol is mentioned.''
Since constants contain no variable occurrences and non-constant expressions must contain at least one variable occurrence, constants come before non-constants in the term order, no matter how large the constants. For example, the list constant
'(monday tuesday wednesday thursday friday)
(+ x 3 (dx i j) (car (reverse klst))) ,
which in translated form is
(binary-+ x (binary-+ '3 (binary-+ (dx i j) (car (reverse klst))))),
will be permuted under the built-in commutativity rules to
(binary-+ '3 (binary-+ x (binary-+ (car (reverse klst)) (dx i j))))
(+ 3 x (car (reverse klst)) (dx i j)).
Two terms with the same numbers of variable occurrences and function
applications and the same pseudo-function application count are ordered by
lexicographic means, based on their structures. See lexorder. Thus,
if two terms
It remains to discuss the notion of pseudo-function application count.
Clearly, two constants are ordered using cases (c) and (d) of term order, since they each contain 0 variable occurrences and no function calls. This raises the question ``How many function applications are in a constant?'' Because we regard the number of function applications as a more fundamental measure of the size of a constant than lexicographic considerations, we decided that for the purposes of term order, constants would be seen as being built by primitive constructor functions. These constructor functions are not actually defined in ACL2 but merely imagined for the purposes of term order. We here use suggestive names for these imagined functions, ignoring entirely the prior use of these names within ACL2. The imagined applications of these functions are what we refer to as pseudo-function applications.
The constant function
(/ (- (s (z))) (s (s (z))))
and contains seven applications. Complex rationals are similarly
constructed from rationals. All character objects are considered primitive
and are constructed by constant functions of the same name. Thus
(p (cs (#\a) (cs (#\b) (o))))
and has six applications. Note that packages are here ignored and thus
Finally, when we refer to the ``pseudo-function application count'', we
mean the number of pseudo-function applications as described above, except
that we bound this number by the constant