SUBVERSIVE-INDUCTIONS

why we restrict encapsulated recursive functions
Major Section:  MISCELLANEOUS

See subversive-recursions.















































































SUBVERSIVE-RECURSIONS

why we restrict encapsulated recursive functions
Major Section:  MISCELLANEOUS

Subtleties arise when one of the ``constrained'' functions, f, introduced in the signature of an encapsulate event, is involved in the termination argument for a non-local recursively defined function, g, in that encapsulate. During the processing of the encapsulated events, f is locally defined to be some witness function, f'. Properties of f' are explicitly proved and exported from the encapsulate as the constraints on the undefined function f. But if f is used in a recursive g defined within the encapsulate, then the termination proof for g may use properties of f' -- the witness -- that are not explicitly set forth in the constraints stated for f.

Such recursive g are said be ``subversive'' because if naively treated they give rise to unsound induction schemes or (via functional instantiation) recurrence equations that are impossible to satisfy. We illustrate what could go wrong below.

Subversive recursions are not banned outright. Instead, they are treated as part of the constraint. That is, in the case above, the definitional equation for g becomes one of the constraints on f. This is generally a severe restriction on future functional instantiations of f. In addition, ACL2 removes from its knowledge of g any suggestions about legal inductions to ``unwind'' its recursion.

What should you do? Often, the simplest response is to move the offending recursive definition, e.g., g, out of the encapsulate. That is, introduce f by constraint and then define g as an ``independent'' event. You may need to constrain ``additional'' properties of f in order to admit g, e.g., constrain it to reduce some ordinal measure. However, by separating the introduction of f from the admission of g you will clearly identify the necessary constraints on f, functional instantiations of f will be simpler, and g will be a useful function which suggests inductions to the theorem prover.

Note that the functions introduced in the signature should not even occur ancestrally in the termination proofs for non-local recursive functions in the encapsulate. That is, the constrained functions of an encapsulate should not be reachable in the dependency graph of the functions used in the termination arguments of recursive functions in encapsulate. If they are reachable, their definitions become part of the constraints.

The following event illustrates the problem posed by subversive recursions.

(encapsulate ((f (x) t))
  (local (defun f (x) (cdr x)))
  (defun g (x)
    (if (consp x) (not (g (f x))) t)))
Suppose, contrary to how ACL2 works, that the encapsulate above were to introduce no constraints on f on the bogus grounds that the only use of f in the encapsulate is in an admissible function. We discuss the plausibility of this bogus argument in a moment.

Then it would be possible to prove the theorem:

(defthm f-not-identity
  (not (equal (f '(a . b)) '(a . b)))
  :rule-classes nil
  :hints (("Goal" :use (:instance g (x '(a . b))))))
simply by observing that if (f '(a . b)) were '(a . b), then (g '(a . b)) would be (not (g '(a . b))), which is impossible.

But then we could functionally instantiate f-not-identity, replacing f by the identity function, to prove nil! This is bad.

(defthm bad
  nil
  :rule-classes nil
  :hints
  (("Goal" :use (:functional-instance f-not-identity (f identity)))))
This sequence of events was legal in versions of ACL2 prior to Version 1.5. When we realized the problem we took steps to make it illegal. However, our steps were insufficient and it was possible to sneak in a subversive function (via mutual recursion) as late as Version 2.3.

We now turn to the plausibility of the bogus argument above. Why might one even be tempted to think that the definition of g above poses no constraint on f? Here is a very similar encapsulate.

(encapsulate ((f (x) t))
  (local (defun f (x) (cdr x)))
  (defun map (x)
    (if (consp x)
        (cons (f x) (map (cdr x)))
      nil)))
Here map plays the role of g above. Like g, map calls the constrained function f. But map truly does not constrain f. In particular, the definition of map could be moved ``out'' of the encapsulate so that map is introduced afterwards. The difference between map and g is that the constrained function plays no role in the termination argument for the one but does for the other.

As a ``user-friendly'' gesture, ACL2 implicitly moves map-like functions out of encapsulations; logically speaking, they are introduced after the encapsulation. This simplifies the constraint. This is done only for ``top-level'' encapsulations. When an encapsulate containing a non-empty signature is embedded in another encapsulate with a non-empty signature, no attempt is made to move map-like functions out. The user is advised, via the ``infected'' warning, to phrase the encapsulation in the simplest way possible.

The lingering bug between Versions 1.5 and 2.3 mentioned above was due to our failure to detect the g-like nature of some functions when they were defined in mutually recursively cliques with other functions. The singly recursive case was recognized. The bug arose because our detection ``algorithm'' was based on the ``suggested inductions'' left behind by successful definitions. We failed to recall that mutually-recursive definitions do not, as of this writing, make any suggestions about inductions and so did not leave any traces of their subversive natures.













































































SYNTAX

the syntax of ACL2 is that of Common Lisp
Major Section:  MISCELLANEOUS

For the details of ACL2 syntax, see CLTL. For examples of ACL2 syntax, use :pe to print some of the ACL2 system code. For example:

:pe assoc-equal
:pe dumb-occur
:pe fn-var-count
:pe add-linear-variable-to-alist

There is no comprehensive description of the ACL2 syntax yet, except that found in CLTL. Also see term.













































































SYNTAXP

to attach a heuristic filter on a :rewrite rule
Major Section:  MISCELLANEOUS

Example:
Consider the :REWRITE rule created from

(IMPLIES (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))) (EQUAL (LXD X) (LXD (NORM X)))).

The syntaxp hypothesis in this rule will allow the rule to be applied to (lxd (trn a b)) but will not allow it to be applied to (lxd (norm a)).

General Form:
(SYNTAXP test)
may be used as the nth hypothesis in a :rewrite rule whose :corollary is (implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs)) provided test is a term, test contains at least one variable, and every variable occuring freely in test occurs freely in lhs or in some hypi, i<n. Formally, syntaxp is a function of one argument; syntaxp always returns t and so may be added as a vacuous hypothesis. However, the test ``inside'' the syntaxp form is actually treated as a meta-level proposition about the proposed instantiation of the rule's variables and that proposition must evaluate to true (non-nil) to ``establish'' the syntaxp hypothesis.

We illustrate this by slightly elaborating the example given above. Consider a :rewrite rule whose :corollary is:

(IMPLIES (AND (RATIONALP X)
              (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))))
         (EQUAL (LXD X) (LXD (NORM X))))
How is this rule applied to (lxd (trn a b))? First, we form a substitution that instantiates the left-hand side of the conclusion of the rule so that it is identical to the target term. In the present case, the substitution replaces x with (trn a b). Then we backchain to establish the hypotheses, in order. Ordinarily this means that we instantiate each hypothesis with our substitution and then attempt to rewrite the resulting instance to true. Of course, most users are aware of some exceptions to this general rule. For example, if a hypothesis contains a ``free-variable'' -- one not bound by the current substitution -- we attempt to extend the substitution by searching for an instance of the hypothesis among known truths. Forced hypotheses are another exception to the general rule of how hypotheses are relieved. Hypotheses marked with syntaxp, as in (syntaxp test), are also exceptions. Instead of instantiating the hypothesis and trying to establish it, we evaluate test in an environment in which its variable symbols are bound to the quotations of the terms to which those variables are bound in the instantiating substitution. In the case in point, we evaluate the test
 (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))
in an environment where x is bound to '(trn a b), i.e., the list of length three whose car is the symbol 'trn. Thus, the test returns t because x is a consp and its car is not the symbol 'norm. When the syntaxp test evaluates to t, we consider the syntaxp hypothesis to have been established; this is sound because (syntaxp test) is t regardless of test. If the test evaluates to nil (or fails to evaluate because of guard violations) we act as though we cannot establish the hypothesis and abandon the attempt to apply the rule; it is always sound to give up.

Note that the test of a syntaxp hypothesis does not deal with the meaning or semantics or values of the terms but with their syntactic forms. In the example above, the syntaxp hypothesis allows the rule to be applied to every target of the form (lxd u), provided (rationalp u) can be established and u is not of the form (norm v). Observe that without this syntactic restriction the rule above could loop producing a sequence of increasingly complex targets (lxd a), (lxd (norm a)), (lxd (norm (norm a))), etc. An intuitive reading of the rule might be ``norm the argument of lxd (when it is rationalp) unless it has already been normed.''

Another common syntactic restriction is

  (SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE))).
A rule with such a hypothesis can be applied only if x is bound to a specific constant. Thus, if x is 23 (which is actually represented internally as (quote 23)), the test evaluates to t; but if x is (+ 11 12) it evaluates to nil (because (car x) is the symbol '+). It is often desirable to delay the application of a rule until certain subterms are in some kind of normal form so that the application doesn't produce excessive case splits.













































































TERM

the three senses of well-formed ACL2 expressions or formulas
Major Section:  MISCELLANEOUS

Examples of Terms:
(cond ((caar x) (cons t x)) (t 0))   ; an untranslated term

(if (car (car x)) (cons 't x) '0) ; a translated term

(car (cons x y) 'nil v) ; a pseudo-term

In traditional first-order predicate calculus a ``term'' is a syntactic entity denoting some object in the universe of individuals. Often, for example, the syntactic characterization of a term is that it is either a variable symbol or the application of a function symbol to the appropriate number of argument terms. Traditionally, ``atomic formulas'' are built from terms with predicate symbols such as ``equal'' and ``member;'' ``formulas'' are then built from atomic formulas with propositional ``operators'' like ``not,'' ``and,'' and ``implies.'' Theorems are formulas. Theorems are ``valid'' in the sense that the value of a theorem is true, in any model of the axioms and under all possible assignments of individuals to variables.

However, in ACL2, terms are used in place of both atomic formulas and formulas. ACL2 does not have predicate symbols or propositional operators as distinguished syntactic entities. The ACL2 universe of individuals includes a ``true'' object (denoted by t) and a ``false'' object (denoted by nil), predicates and propositional operators are functions that return these objects. Theorems in ACL2 are terms and the ``validity'' of a term means that, under no assignment to the variables does the term evaluate to nil.

We use the word ``term'' in ACL2 in three distinct senses. We will speak of ``translated'' terms, ``untranslated'' terms, and ``pseudo-'' terms.

Translated Terms: The Strict Sense and Internal Form

In its most strict sense, a ``term'' is either a legal variable symbol, a quoted constant, or the application of an n-ary function symbol or closed lambda expression to a true list of n terms.

The legal variable symbols are symbols other than t or nil which are not in the keyword package, do not start with ampersand, do not start and end with asterisks, and if in the main Lisp package, do not violate an appropriate restriction (see name).

Quoted constants are expressions of the form (quote x), where x is any ACL2 object. Such expressions may also be written 'x.

Closed lambda expressions are expressions of the form (lambda (v1 ... vn) body) where the vi are distinct legal variable symbols, body is a term, and the only free variables in body are among the vi.

The function termp, which takes two arguments, an alleged term x and a logical world w (see world), recognizes terms of a given extension of the logic. Termp is defined in :program mode. Its definition may be inspected with :pe termp for a complete specification of what we mean by ``term'' in the most strict sense. Most ACL2 term-processing functions deal with terms in this strict sense and use termp as a guard. That is, the ``internal form'' of a term satisfies termp, the strict sense of the word ``term.''

Untranslated Terms: What the User Types

While terms in the strict sense are easy to explore (because their structure is so regular and simple) they can be cumbersome to type. Thus, ACL2 supports a more sugary syntax that includes uses of macros and constant symbols. Very roughly speaking, macros are functions that produce terms as their results. Constants are symbols that are associated with quoted objects. Terms in this sugary syntax are ``translated'' to terms in the strict sense; the sugary syntax is more often called ``untranslated.'' Roughly speaking, translation just implements macroexpansion, the replacement of constant symbols by their quoted values, and the checking of all the rules governing the strict sense of ``term.''

More precisely, macro symbols are as described in the documentation for defmacro. A macro, mac, can be thought of as a function, mac-fn, from ACL2 objects to an ACL2 object to be treated as an untranslated term. For example, caar is defined as a macro symbol; the associated macro function maps the object x into the object (car (car x)). A macro form is a ``call'' of a macro symbol, i.e., a list whose car is the macro symbol and whose cdr is an arbitrary true list of objects, used as a term. Macroexpansion is the process of replacing in an untranslated term every occurrence of a macro form by the result of applying the macro function to the appropriate arguments. The ``appropriate'' arguments are determined by the exact form of the definition of the macro; macros support positional, keyword, optional and other kinds of arguments. See defmacro.

In addition to macroexpansion and constant symbol dereferencing, translation implements the mapping of let and let* forms into applications of lambda expressions and closes lambda expressions containing free variables. Thus, the translation of

(let ((x (1+ i))) (cons x k))
can be seen as a two-step process that first produces
((lambda (x) (cons x k)) (1+ i))
and then
((lambda (x k) (cons x k)) (1+ i) k) .
Observe that the body of the let and of the first lambda expression contains a free k which is finally bound and passed into the second lambda expression.

When we say, of an event-level function such as defun or defthm, that some argument ``must be a term'' we mean an untranslated term. The event functions translate their term-like arguments.

To better understand the mapping between untranslated terms and translated terms it is convenient to use the keyword command :trans to see examples of translations. See trans and also see trans1.

Pseudo-Terms: A Common Guard for Metafunctions

Because termp is defined in :program mode, it cannot be used effectively in conjectures to be proved. Furthermore, from the perspective of merely guarding a term processing function, termp often checks more than is required. Finally, because termp requires the logical world as one of its arguments it is impossible to use termp as a guard in places where the logical world is not itself one of the arguments.

For these reasons we support the idea of ``pseudo-terms.'' A pseudo-term is either a symbol (but not necessarily one having the syntax of a legal variable symbol), a true list beginning with quote (but not necessarily well-formed), or the ``application of'' a symbol or pseudo lambda expression to a true list of pseudo-terms. A pseudo lambda expression is an expression of the form (lambda (v1 ... vn) body) where the vi are all symbols and body is a pseudo-term.

Pseudo-terms are recognized by the unary function pseudo-termp. If (termp x w) is true, then (pseudo-termp x) is true. However, if x fails to be a (strict) term it may nevertheless still be a pseudo-term. For example, (car a b) is not a term, because car is applied to the wrong number of arguments, but it is a pseudo-term.

The structures recognized by pseudo-termp can be recursively explored with the same simplicity that terms can be. In particular, if x is not a variablep or an fquotep, then (ffn-symb x) is the function (symbol or lambda expression) and (fargs x) is the list of argument pseudo-terms. A metafunction may use pseudo-termp as the guard.













































































TERM-ORDER

the ordering relation on terms used by ACL2
Major Section:  MISCELLANEOUS

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.

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, and term1 comes before term2 in a certain lexicographic ordering based their structure as Lisp objects.

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)).
Clearly, two constants are ordered using cases (b) and (c) of term order, since they each contain 0 variable occurrences. 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 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?''

Two terms with the same numbers of variable occurrences and function applications are ordered by lexicographic means, based on their structures. In the lexicographic ordering, two atoms are ordered ``alphabetically'' as described below, an atom and a cons are ordered so that the atom comes first, and two conses are ordered so that the one with the recursively smaller car comes first, with the cdrs being compared only if the cars are equal. Thus, if two terms (member ...) and (reverse ...) contain the same numbers of variable occurrences and function applications, 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 only to define what we mean by the alphabetic ordering on Lisp atoms. Within a single type, numbers are compared arithmetically, characters are compared via their (char) codes, and strings and symbols are compared with the conventional alphabetic ordering on sequences of characters. Across types, numbers come before characters, characters before strings, and strings before symbols.













































































TTREE

tag trees
Major Section:  MISCELLANEOUS

Many low-level ACL2 functions take and return ``tag trees'' or ``ttrees'' (pronounced ``tee-trees'') which contain various useful bits of information such as the lemmas used, the linearize assumptions made, etc.

Let a ``tagged pair'' be a list whose car is a symbol, called the ``tag,'' and whose cdr is an arbitrary object, called the ``tagged object.'' A ``tag tree'' is either nil, a tagged pair consed onto a tag tree, or a non-nil tag tree consed onto a tag tree.

Abstractly a tag tree represents a list of sets, each member set having a name given by one of the tags occurring in the ttree. The elements of the set named tag are all of the objects tagged tag in the tree. To cons a tagged pair (tag . obj) onto a tree is to add-to-set-equal obj to the set corresponding to tag. To cons two tag trees together is to union-equal the corresponding sets. The concrete representation of the union so produced has duplicates in it, but we feel free to ignore or delete duplicates.

The beauty of this definition is that to combine two non-nil tag trees you need do only one cons.

The following function accumulates onto ans the set associated with a given tag in a ttree:

(defun tagged-objects (tag ttree ans)
 (cond
  ((null ttree) ans)
  ((symbolp (caar ttree))             ; ttree = ((tag . obj) . ttree)
   (tagged-objects tag (cdr ttree)
                   (cond ((eq (caar ttree) tag)
                          (add-to-set-equal (cdar ttree) ans))
                         (t ans))))
  (t                                  ; ttree = (ttree . ttree)
     (tagged-objects tag (cdr ttree)
                         (tagged-objects tag (car ttree) ans)))))
This function is defined as a :PROGRAM mode function in ACL2.

The rewriter, for example, takes a term and a ttree (among other things), and returns a new term, term', and new ttree, ttree'. Term' is equivalent to term (under the current assumptions) and the ttree' is an extension of ttree. If we focus just on the set associated with the tag LEMMA in the ttrees, then the set for ttree' is the extension of that for ttree obtained by unioning into it all the runes used by the rewrite. The set associated with LEMMA can be obtained by (tagged-objects 'LEMMA ttree nil).













































































TYPE-SET

how type information is encoded in ACL2
Major Section:  MISCELLANEOUS

To help you experiment with type-sets we briefly note the following utility functions.

(type-set-quote x) will return the type-set of the object x. For example, (type-set-quote "test") is 2048 and (type-set-quote '(a b c)) is 512.

(type-set 'term nil nil nil nil (ens state) (w state) nil) will return the type-set of term. For example,

(type-set '(integerp x) nil nil nil nil (ens state) (w state) nil)
will return (mv 192 nil). 192, otherwise known as *ts-boolean*, is the type-set containing t and nil. The second result may be ignored in these experiments. Term must be in the translated, internal form shown by :trans. See trans and see term.

(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil) will return the type-set deduced for the variable symbol x assuming the translated term, term, true. The second result may be ignored in these experiments. For example,

(type-set-implied-by-term 'v nil '(integerp v)
                          (ens state) (w state) nil)
returns 11.

(convert-type-set-to-term 'x ts (ens state) (w state) nil) will return a term whose truth is equivalent to the assertion that the term x has type-set ts. The second result may be ignored in these experiments. For example

(convert-type-set-to-term 'v 523 (ens state) (w state) nil)
returns a term expressing the claim that v is either an integer or a non-nil true-list. 523 is the logical-or of 11 (which denotes the integers) with 512 (which denotes the non-nil true-lists).

The ``actual primitive types'' of ACL2 are listed in *actual-primitive-types*. These primitive types include such types as *ts-zero*, *ts-positive-integer*, *ts-nil* and *ts-proper-consp*. Each actual primitive type denotes a set -- sometimes finite and sometimes not -- of ACL2 objects and these sets are pairwise disjoint. For example, *ts-zero* denotes the set containing 0 while *ts-positive-integer* denotes the set containing all of the positive integers.

The actual primitive types were chosen by us to make theorem proving convenient. Thus, for example, the actual primitive type *ts-nil* contains just nil so that we can encode the hypothesis ``x is nil'' by saying ``x has type *ts-nil*'' and the hypothesis ``x is non-nil'' by saying ``x has type complement of *ts-nil*.'' We similarly devote a primitive type to t, *ts-t*, and to a third type, *ts-non-t-non-nil-symbol*, to contain all the other ACL2 symbols.

Let *ts-other* denote the set of all Common Lisp objects other than those in the actual primitive types. Thus, *ts-other* includes such things as floating point numbers and CLTL array objects. The actual primitive types together with *ts-other* constitute what we call *universe*. Note that *universe* is a finite set containing one more object than there are actual primitive types; that is, here we are using *universe* to mean the finite set of primitive types, not the infinite set of all objects in all of those primitive types. *Universe* is a partitioning of the set of all Common Lisp objects: every object belongs to exactly one of the sets in *universe*.

Abstractly, a ``type-set'' is a subset of *universe*. To say that a term, x, ``has type-set ts'' means that under all possible assignments to the variables in x, the value of x is a member of some member of ts. Thus, (cons x y) has type-set {*ts-proper-cons* *ts-improper-cons*}. A term can have more than one type-set. For example, (cons x y) also has the type-set {*ts-proper-cons* *ts-improper-cons* *ts-nil*}. Extraneous types can be added to a type-set without invalidating the claim that a term ``has'' that type-set. Generally we are interested in the smallest type-set a term has, but because the entire theorem-proving problem for ACL2 can be encoded as a type-set question, namely, ``Does p have type-set complement of *ts-nil*?,'' finding the smallest type-set for a term is an undecidable problem. When we speak informally of ``the'' type-set we generally mean ``the type-set found by our heuristics'' or ``the type-set assumed in the current context.''

Note that if a type-set, ts, does not contain *ts-other* as an element then it is just a subset of the actual primitive types. If it does contain *ts-other* it can be obtained by subtracting from *universe* the complement of ts. Thus, every type-set can be written as a (possibly complemented) subset of the actual primitive types.

By assigning a unique bit position to each actual primitive type we can encode every subset, s, of the actual primitive types by the nonnegative integer whose ith bit is on precisely if s contains the ith actual primitive type. The type-sets written as the complement of s are encoded as the twos-complement of the encoding of s. Those type-sets are thus negative integers. The bit positions assigned to the actual primitive types are enumerated from 0 in the same order as the types are listed in *actual-primitive-types*. At the concrete level, a type-set is an integer between *min-type-set* and *max-type-set*, inclusive.

For example, *ts-nil* has bit position 6. The type-set containing just *ts-nil* is thus represented by 64. If a term has type-set 64 then the term is always equal to nil. The type-set containing everything but *ts-nil* is the twos-complement of 64, which is -65. If a term has type-set -65, it is never equal to nil. By ``always'' and ``never'' we mean under all, or under no, assignments to the variables, respectively.

Here is a more complicated example. Let s be the type-set containing all of the symbols and the natural numbers. The relevant actual primitive types, their bit positions and their encodings are:

actual primitive type       bit    value

*ts-zero* 0 1 *ts-positive-integer* 1 2 *ts-nil* 6 64 *ts-t* 7 128 *ts-non-t-non-nil-symbol* 8 256

Thus, the type-set s is represented by (+ 1 2 64 128 256) = 451. The complement of s, i.e., the set of all objects other than the natural numbers and the symbols, is -452.