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.

THE-METHOD

Major Section:  MISCELLANEOUS

Many users develop proof scripts in an Emacs buffer and submit one event at a time to the theorem prover running in a *shell* buffer. The script buffer is logically divided into two regions: the events that have been accepted by the theorem prover and those that have not yet been accepted. An imaginary ``barrier'' divides these two regions. The region above the barrier describes the state of the *shell* buffer (and ACL2's logical world). The region below the barrier is the ``to do'' list.

We usually start a proof project by typing the key lemmas, and main goal into the to do list. Definitions are here just regarded as theorems to prove (i.e., the measure conjectures). Then we follow ``The Method.''

(1) Think about the proof of the first theorem in the to do list. Structure the proof either as an induction followed by simplification or just simplification. Have the necessary lemmas been proved? That is, are the necessary lemmas in the done list already? If so, proceed to Step 2. Otherwise, add the necessary lemmas at the front of the to do list and repeat Step 1.

(2) Call the theorem prover on the first theorem in the to do list and let the output stream into the *shell* buffer. Abort the proof if it runs more than a few seconds.

(3) If the theorem prover succeeded, advance the barrier past the successful command and go to Step 1.

(4) Otherwise, inspect the failed proof attempt, starting from the beginning, not the end. Basically you should look for the first place the proof attempt deviates from your imagined proof. If your imagined proof was inductive, inspect the induction scheme used by ACL2. If that is ok, then find the first subsequent subgoal that is stable under simplification and think about why it was not proved by the simplifier. If your imagined proof was not inductive, then think about the first subgoal stable under simplification, as above. Modify the script appropriately. It usually means adding lemmas to the to do list, just in front of the theorem just tried. It could mean adding hints to the current theorem. In any case, after the modifications go to Step 1.

We do not seriously suggest that this or any rotely applied algorithm will let you drive ACL2 to difficult proofs. Indeed, to remind you of this we call this ``The Method'' rather than ``the method.'' That is, we are aware of the somewhat pretentious nature of any such advice. But these remarks have helped many users approach ACL2 in a constructive and disciplined way.

We say much more about The Method in the ACL2 book. See the home page.

Learning to read failed proofs is a useful skill. There are several kinds of ``checkpoints'' in a proof: (1) a formula to which induction is being (or would be) applied, (2) the first formula stable under simplification, (3) a formula that is possibly generalized, either by cross-fertilizing with and throwing away an equivalence hypothesis or by explicit generalization of a term with a new variable.

At the induction checkpoint, confirm that you believe the formula being proved is a theorem and that it is appropriately strong for an inductive proof. Read the selected induction scheme and make sure it agrees with your idea of how the proof should go.

At the post-simplification checkpoint, which is probably the most commonly seen, consider whether there are additional rewrite rules you could prove to make the formula simplify still further. Look for compositions of function symbols you could rewrite. Look for contradictions among hypotheses and prove the appropriate implications: for example, the checkpoint might contain the two hypotheses (P (F A)) and (NOT (Q (G (F A)))) and you might realize that (implies (p x) (q (g x))) is a theorem. Look for signs that your existing rules did not apply, e.g., for terms that should have been rewritten, and figure out why they were not. Possible causes include that they do not exactly match your old rules, that your old rules have hypotheses that cannot be relieved here -- perhaps because some other rules are missing, or perhaps your old rules are disabled. If you cannot find any further simplifications to make in the formula, ask yourself whether it is valid. If so, sketch a proof. Perhaps the proof is by appeal to a combination of lemmas you should now prove?

At the two generalization checkpoints --- where hypotheses are discarded or terms are replaced by variables --- ask yourself whether the result is a theorem. It often is not. Think about rewrite rules that would prove the formula. These are often restricted versions of the overly-general formulas created by the system's heuristics.

See proof-tree for a discussion of a tool to help you navigate through ACL2 proofs.