Major Section: ACL2-BUILT-INS

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.

`Term1`

comes before `term2`

in the term order iff

(a) the number of variable occurrences in

`term1`

is 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

`term1`

is 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

`term1`

is 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

`term1`

comes before`term2`

in a lexicographic ordering,`lexorder`

, based their structure as Lisp objects: see lexorder.

The function `term-order`

, when applied to the translations of two
ACL2 terms, returns `t`

iff the first is ``less than or equal'' to the
second in the term order.

By ``number of variable occurrences'' we do not mean ``number of distinct
variables'' but ``number of times a variable symbol is mentioned.''
`(Cons x x)`

has two variable occurrences, not one. Thus, perhaps
counterintuitively, a large term that contains only one variable occurrence,
e.g., `(standard-char-p (car (reverse x)))`

comes before `(cons x x)`

in
the term order.

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)comes before

`x`

in the term order. Because term order is involved in the
control of permutative rewrite rules and used to shift smaller terms to the
left, a set of permutative rules designed to allow the permutation of any two
tips in a tree representing the nested application of some function will
always move the constants into the left-most tips. Thus,
(+ x 3 (car (reverse klst)) (dx i j)) ,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))))or

(+ 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

`(member ...)`

and `(reverse ...)`

contain the same numbers of
variable occurrences and function applications, and no quoted constants, then
the `member`

term is first in the term order because `member`

comes
before `reverse`

in the term order (which is here reduced to alphabetic
ordering).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 `z`

constructs `0`

. Positive integers are
constructed from `(z)`

by the successor function, `s`

. Thus `2`

is
`(s (s (z)))`

and contains three function applications. `100`

contains
one hundred and one applications. Negative integers are constructed from
their positive counterparts by `-`

. Thus, `-2`

is `(- (s (s (z))))`

and has four applications. Ratios are constructed by the dyadic function
`/`

. Thus, `-1/2`

is

(/ (- (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

`#\a`

and
`#\b`

both contain one application. Strings are built from the empty
string, `(o)`

by the ``string-cons'' function written `cs`

. Thus
`"AB"`

is `(cs (#\a) (cs (#\b) (o)))`

and contains five applications.
Symbols are obtained from strings by ``packing'' the `symbol-name`

with
the unary function `p`

. Thus `'ab`

is
(p (cs (#\a) (cs (#\b) (o))))and has six applications. Note that packages are here ignored and thus

`'acl2::ab`

and `'my-package::ab`

each contain just six applications.
Finally, conses are built with `cons`

, as usual. So `'(1 . 2)`

is
`(cons '1 '2)`

and contains six applications, since `'1`

contains two and
`'2`

contains three. This, for better or worse, answers the question ``How
many function applications are in a constant?''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 `(fn-count-evg-max-val)`

. (This bound is
important for efficiency, so that constants that are very large `cons`

structures do not cause significant slowdown as ACL2 attempts to walk through
them while computing their pseudo-function application count.)