STATE

Major Section:  MISCELLANEOUS

The ACL2 state object is used extensively in programming the ACL2 system, and has been used in other ACL2 programs as well. However, most users, especially those interested in specification and verification (as opposed to programming per se), need not be aware of the role of the state object in ACL2, and will not write functions that use it explicitly. We say more about this point at the end of this documentation topic.

The ACL2 state object is an example of a single-threaded object or stobj. ACL2 allows the user to define new single-threaded objects. Generally, the ACL2 may need to access the ACL2 state but should not (cannot) change it except via a certain set of approved functions such as defun and defthm. If you need a state-like object to which you have complete rights, you may want a stobj.

Key to the idea of our state is the notion of single-threadedness. This is explained in see stobj. The upshot of it is that state is a variable symbol with severe restrictions on its use, so that it can be passed into only certain functions in certain slots, and must be returned by those functions that ``modify'' it. Henceforth, we do not discuss single-threaded objects in general (which the user can introduce with defstobj) but one in particular, namely ACL2's state object.

The global table is perhaps the most visible portion of the state object. Using the interface functions @ and assign, a user may bind global variables to the results of function evaluations (much as an Nqthm user exploits the Nqthm utility r-loop). See @ and see assign.

ACL2 supports several facilities of a truly von Neumannesque state machine character, including file io and global variables. Logically speaking, the state is a true list of the 14 components described below. There is a ``current'' state object at the top-level of the ACL2 command loop. This object is understood to be the value of what would otherwise be the free variable state appearing in top-level input. When any command returns a state object as one of its values, that object becomes the new current state. But ACL2 provides von Neumann style speed for state operations by maintaining only one physical (as opposed to logical) state object. Operations on the state are in fact destructive. This implementation does not violate the applicative semantics because we enforce certain draconian syntactic rules regarding the use of state objects. For example, one cannot ``hold on'' to an old state, access the components of a state arbitrarily, or ``modify'' a state object without passing it on to subsequent state-sensitive functions.

Every routine that uses the state facilities (e.g. does io, or calls a routine that does io), must be passed a ``state object.'' And a routine must return a state object if the routine modifies the state in any way. Rigid syntactic rules governing the use of state objects are enforced by the function translate, through which all ACL2 user input first passes. State objects can only be ``held'' in the formal parameter state, never in any other formal parameter and never in any structure (excepting a multiple-values return list field which is always a state object). State objects can only be accessed with the primitives we specifically permit. Thus, for example, one cannot ask, in code to be executed, for the length of state or the car of state. In the statement and proof of theorems, there are no syntactic rules prohibiting arbitrary treatment of state objects.

Logically speaking, a state object is a true list whose members are as follows:

Open-input-channels, an alist with keys that are symbols in package "ACL2-INPUT-CHANNEL". The value (cdr) of each pair has the form ((:header type file-name open-time) . elements), where type is one of :character, :byte, or :object and elements is a list of things of the corresponding type, i.e. characters, integers of type (mod 255), or lisp objects in our theory. File-name is a string. Open-time is an integer. See io.

Open-output-channels, an alist with keys that are symbols in package "ACL2-OUTPUT-CHANNEL". The value of a pair has the form ((:header type file-name open-time) . current-contents). See io.

Global-table, an alist associating symbols (to be used as ``global variables'') with values. See @, and see assign.

T-stack, a list of arbitrary objects accessed and changed by the functions aref-t-stack and aset-t-stack.

32-bit-integer-stack, a list of arbitrary 32-bit-integers accessed and changed by the functions aref-32-bit-integer-stack and aset-32-bit-integer-stack.

Big-clock-entry, an integer, that is used logically to bound the amount of effort spent to evaluate a quoted form.

Idates, a list of dates and times, used to implement the function print-current-idate, which prints the date and time.

Run-times, a list of integers, used to implement the functions that let ACL2 report how much time was used, but inaccessible to the user.

File-clock, an integer that is increased on every file opening and closing and used to maintain the consistency of the io primitives.

Readable-files, an alist whose keys have the form (string type time), where string is a file name and time is an integer. The value associated with such a key is a list of characters, bytes, or objects, according to type. The time field is used in the following way: when it comes time to open a file for input, we will only look for a file of the specified name and type whose time field is that of file-clock. This permits us to have a ``probe-file'' aspect to open-file: one can ask for a file, find it does not exist, but come back later and find that it does now exist.

Written-files, an alist whose keys have the form (string type time1 time2), where string is a file name, type is one of :character, :byte or :object, and time1 and time2 are integers. Time1 and time2 correspond to the file-clock time at which the channel for the file was opened and closed. This field is write-only; the only operation that affects this field is close-output-channel, which conses a new entry on the front.

Read-files, a list of the form (string type time1 time2), where string is a file name and time1 and time2 were the times at which the file was opened for reading and closed. This field is write only.

Writeable-files, an alist whose keys have the form (string type time). To open a file for output, we require that the name, type, and time be on this list.

List-all-package-names-lst, a list of true-listps. Roughly speaking, the car of this list is the list of all package names known to this Common Lisp right now and the cdr of this list is the value of this state variable after you look at its car. The function, list-all-package-names, which takes the state as an argument, returns the car and cdrs the list (returning a new state too). This essentially gives ACL2 access to what is provided by CLTL's list-all-packages. Defpkg uses this feature to insure that the about-to-be-created package is new in this lisp. Thus, for example, in akcl it is impossible to create the package "COMPILER" with defpkg because it is on the list, while in Lucid that package name is not initially on the list.

We recommend avoiding the use of the state object when writing ACL2 code intended to be used as a formal model of some system, for several reasons. First, the state object is complicated and contains many components that are oriented toward implementation and are likely to be irrelevant to the model in question. Second, there is currently not much support for reasoning about ACL2 functions that manipulate the state object, beyond their logical definitions. Third, the documentation about state is not as complete as one might wish.

User-defined single-threaded objects offer the speed of state while giving the user complete access to all the fields. See stobj.

SUBVERSIVE-INDUCTIONS

Major Section:  MISCELLANEOUS

See subversive-recursions.

SUBVERSIVE-RECURSIONS

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 *) => *))
  (local (defun f (x) (cdr x)))
  (defun g (x)
    (if (consp x) (not (g (f x))) t)))

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

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

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 *) => *))
  (local (defun f (x) (cdr x)))
  (defun map (x)
    (if (consp x)
        (cons (f x) (map (cdr x)))
      nil)))

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 list is embedded in another encapsulate with a non-empty signature list, 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

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

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)))).

General Form:
(SYNTAXP test)

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

 (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))

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))).

TERM

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

((lambda (x) (cons x k)) (1+ i))

((lambda (x k) (cons x k)) (1+ i) k) .

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

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.

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)

(+ x 3 (car (reverse klst)) (dx i j)) ,

(binary-+ x
          (binary-+ '3
                    (binary-+ (dx i j)
                              (car (reverse klst))))),

(binary-+ '3
          (binary-+ x
                    (binary-+ (car (reverse klst))
                              (dx i j))))

(+ 3 x (car (reverse klst)) (dx i j)).

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

(p (cs (#\a) (cs (#\b) (o))))

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

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

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

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)

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

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

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