PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS

Major Section:  MISCELLANEOUS

Suppose (defpkg "pkg" imports) is the most recently executed successful definition of "pkg" in this ACL2 session and that it has since been undone, as by :ubt. Any future attempt in this session to define "pkg" as a package must specify an identical imports list.

The restriction stems from the need to implement the reinstallation of saved logical worlds as in error recovery and the :oops command. Suppose that the new defpkg attempts to import some symbol, a::sym, not imported by the previous definition of "pkg". Because it was not imported in the original package, the symbol pkg::sym, different from a::sym, may well have been created and may well be used in some saved worlds. Those saved worlds are Common Lisp objects being held for you ``behind the scenes.'' In order to import a::sym into "pkg" now we would have to unintern pkg::sym, rendering those saved worlds ill-formed. It is because of saved worlds that we do not actually clear out a package when it is undone.

At one point we thought it was sound to allow the new defpkg to import a subset of the old. But that is incorrect. Suppose the old definition of "pkg" imported a::sym but the new one does not. Suppose we allowed that and implemented it simply by setting the imports of "pkg" to the new subset. Then consider the conjecture (eq a::sym pkg::sym). This ought not be a theorem because we did not import a::sym into "pkg". But in fact in AKCL it is a theorem because pkg::sym is read as a::sym because of the old imports.

PRINT-DOC-START-COLUMN

Major Section:  MISCELLANEOUS

Examples:
(assign print-doc-start-column nil)
(assign print-doc-start-column 17)

This state global variable controls the column in which the ``one-liner'' of a formatted documentation string is printed. Generally, when :doc is used to print a documentation string, the name of the documented concept is printed and then :doc tabs over to print-doc-start-column and prints the one-liner. If the name extends past the desired column, :doc outputs a carriage return and then tabs over to the column. If print-doc-start-column is nil, :doc just starts the one-liner two spaces from the end of the name, on the same line. The initial value of print-doc-start-column is 15.

PROMPT

Major Section:  MISCELLANEOUS

The prompt printed by ACL2 conveys information about various ``modes.'' See default-print-prompt and see ld-prompt for details.

PROOF-OF-WELL-FOUNDEDNESS

Major Section:  MISCELLANEOUS

The soundness of ACL2 rests in part on the well-foundedness of e0-ord-< on e0-ordinalps. This can be taken as obvious if one is willing to grant that those concepts are simply encodings of the standard mathematical notions of the ordinals below epsilon-0 and its natural ordering relation. But it is possible to prove that e0-ord-< is well-founded on e0-ordinalps without having to assert any connection to the ordinals and that is what we do here.

We first observe three facts about e0-ord-< on ordinals that have been proved by ACL2 using only structural induction on lists. These theorems can be proved by hand.

(defthm transitivity-of-ord-<
  (implies (and (e0-ord-< x y)
                (e0-ord-< y z))
           (e0-ord-< x z))
  :rule-classes nil)


(defthm non-circularity-of-ord-<
  (implies (e0-ord-< x y)
           (not (e0-ord-< y x)))
  :rule-classes nil)


(defthm trichotomy-of-ord-<
  (implies (and (e0-ordinalp x)
                (e0-ordinalp y))
           (or (equal x y)
               (e0-ord-< x y)
               (e0-ord-< y x)))
  :rule-classes nil)

(defun e0-ord-<= (x y)
  (or (equal x y) (e0-ord-< x y)))

(defthm antisymmetry-of-ord-<=
  (implies (and (e0-ordinalp x)
                (e0-ordinalp y)
                (e0-ord-<= x y)
                (e0-ord-<= y x))
           (equal x y))
  :rule-classes nil
  :hints (("Goal" :use non-circularity-of-ord-<)))


(defthm transitivity-of-e0-ord-<=
  (implies (and (e0-ord-<= x y)
                (e0-ord-<= y z))
           (e0-ord-<= x z))
  :rule-classes nil
  :hints (("Goal" :use transitivity-of-ord-<)))


(defthm trichotomy-of-e0-ord-<
  (implies (and (e0-ordinalp x)
                (e0-ordinalp y))
           (or (e0-ord-<= x y)
               (e0-ord-<= y x)))
  :rule-classes nil
  :hints (("Goal" :use trichotomy-of-ord-<)))

(defun od (l) (if (atom l) 0 (1+ (od (car l)))))

(defthm od-implies-ordlessp
  (implies (< (od x) (od y))
           (e0-ord-< x y)))

Lemma Main. For each non-negative integer n, e0-ord-< well-orders the set of e0-ordinalps with od less than or equal to n .

 Base Case.  n = 0.  The e0-ordinalps with 0 od are the non-negative
 integers.  On the non-negative integers, e0-ord-< is the same as <.


 Induction Step.  n > 0.  We assume that e0-ord-< well-orders the
 e0-ordinalps with od less than n.


   If e0-ord-< does not well-order the e0-ordinalps with od less
   than or equal to n, consider, D, the set of infinite, e0-ord-<
   descending sequences of e0-ordinalps of od less than or equal to n.
   The first element of a sequence in D has od n.  Therefore, the car
   of the first element of a sequence in D has od n-1.  Since
   e0-ord-<, by IH, well-orders the e0-ordinalps with od less than n,
   the set of cars of first elements of the sequences in D has a
   minimal element, which we denote by B and which has od of n-1.


  Let k be the least integer such that for some infinite,
  e0-ord-< descending sequence s of e0-ordinalps with od less than
  or equal to n, the first element of s begins with k occurrences
  of B but not k+1 occurrences of B. Notice that k is positive.


    Having fixed B and k, let s = s(1), s(2), ... be an infinite,
    e0-ord-< descending sequence of e0-ordinalps with od less than
    or equal to n such that B occurs exactly k times at the
    beginning of s(1).


       B occurs exactly k times at the beginning of each s(i).  For
       suppose that s(j) is the first member of s with exactly m
       occurrences of B at the beginning, m /= k.  If m = 0, then
       the car of s(j) has od n-1 (otherwise, by IH, s would not be
       infinite) and the car of s(j) is e0-ord-< B, contradicting
       the minimality of B.  If 0 < m < k, then the fact that the
       sequence beginning at s(j) is infinitely descending
       contradicts the minimality of k.  If m > k, then s(j) is
       greater than its predecessor, which has only k occurrences of
       B at the beginning; but this contradicts the fact that s is
       descending.


       Let t = t(1), t(2), ... be the sequence of e0-ordinalps that
       is obtained by letting t(i) be the result of removing B from
       the front of s(i) exactly k times.  t is infinitely
       descending.  Furthermore, t(1) begins with an e0-ordinalp B'
       that is e0-ord-< B.  Since t is in D, t(1) has od n,
       therefore, B' has od n-1.  But this contradicts the
       minimality of B. Q.E.D.

PSEUDO-TERMP

Major Section:  MISCELLANEOUS

Example Forms:
(pseudo-termp '(car (cons x 'nil)))      ; has value t
(pseudo-termp '(car x y z))              ; also has value t!
(pseudo-termp '(delta (h x)))            ; has value t
(pseudo-termp '(delta (h x) . 7))        ; has value nil (not a true-listp)
(pseudo-termp '((lambda (x) (car x)) b)) ; has value t
(pseudo-termp '(if x y 123))             ; has value nil (123 is not quoted)
(pseudo-termp '(if x y '123))            ; has value t

See term for a discussion of the various meanings of the word ``term'' in ACL2. 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 n terms. By ``legal variable symbol'' we exclude constant symbols, such as t, nil, and *ts-rational*. By ``quoted constants'' we include 't (aka (quote t)), 'nil, '31, etc., and exclude constant names such as t, nil and *ts-rational*, unquoted constants such as 31 or 1/2, and ill-formed quote expressions such as (quote 3 4). By ``closed lambda expression'' we exclude expressions, such as (lambda (x) (cons x y)), containing free variables in their bodies. Terms typed by the user are translated into strict terms for internal use in ACL2.

The predicate termp checks this strict sense of ``term'' with respect to a given ACL2 logical world; See world. Many ACL2 functions, such as the rewriter, require certain of their arguments to satisfy termp. However, as of this writing, termp is in :program mode and thus cannot be used effectively in conjectures to be proved. Furthermore, if regarded simply from the perspective of an effective guard for a term-processing function, termp checks many irrelevant things. (Does it really matter that the variable symbols encountered never start and end with an asterisk?) For these reasons, we have introduced the notion of a ``pseudo-term'' and embodied it in the predicate pseudo-termp, which is easier to check, does not require the logical world as input, has :logic mode, and is often perfectly suitable as a guard on term-processing functions.

A pseudo-termp is either a symbol, a true list of length 2 beginning with the word quote, the application of an n-ary pseudo-lambda expression to a true list of n pseudo-terms, or the application of a symbol to a true list of n pseudo-termps. By an ``n-ary pseudo-lambda expression'' we mean an expression of the form (lambda (v1 ... vn) pterm), where the vi are symbols (but not necessarily distinct legal variable symbols) and pterm is a pseudo-termp.

Metafunctions may use pseudo-termp as a guard.

REDEF

Major Section:  MISCELLANEOUS

Example and General Form:
ACL2 !>:redef

As explained elsewhere (see ld-redefinition-action), this allows redefinition of functions and other events without undoing. A query will be made every time a redefinition is commanded; the user must explicitly acknowledge that the redefinition is intentional. It is possible to set ld-redefinition-action so that the redefinition of non-system functions occurs quietly. See ld-redefinition-action.

REDEF!

Major Section:  MISCELLANEOUS

Example and General Form:
ACL2 !>:redef!
ACL2 p!>

This is the ACL2 system hacker's redefinition command. Note that even system functions can be redefined with a mere warning. Be careful!

REDEFINED-NAMES

Major Section:  MISCELLANEOUS

Example and General Forms:
(redefined-names state)

This function collects names that have been redefined in the current ACL2 state. :Program mode functions that were reclassified to :logic functions are not collected, since such reclassification cannot imperil soundness because it is allowed only when the new and old definitions are identical.

Thus, if (redefined-names state) returns nil then no unsafe definitions have been made, regardless of ld-redefinition-action. See ld-redefinition-action.

REDUNDANT-EVENTS

Major Section:  MISCELLANEOUS

Sometimes an event will announce that it is ``redundant''. When this happens, no change to the logical world has occurred. This happens when the logical name being defined is already defined and has exactly the same definition, from the logical point of view. This feature permits two independent books, each of which defines some name, to be included sequentially provided they use exactly the same definition.

When are two logical-name definitions considered exactly the same? It depends upon the kind of name being defined.

A deflabel event is never redundant. This means that if you have a deflabel in a book and that book has been included (without error), then references to that label denote the point in history at which the book introduced the label. See the note about shifting logical names, below.

A defun or mutual-recursion (or defuns) event is redundant if for each function to be introduced, there has already been introduced a function with the same name, the same formals, and syntactically identical guard, type declarations, and body (before macroexpansion).

A verify-guards event is redundant if the function has already had its guards verified.

A defaxiom or defthm event is redundant if there is already an axiom or theorem of the given name and both the formula (after macroexpansion) and the rule-classes are syntactically identical. Note that a defaxiom can make a subsequent defthm redundant, and a defthm can make a subsequent defaxiom redundant as well.

A defconst is redundant if the name has been defined to have the same value.

A defstobj is never redundant. Blah blah...

A defmacro is redundant if there is already a macro defined with the same name and syntactically identical arguments, guard, and body.

A defpkg is redundant if a package of the same name with exactly the same imports has been defined.

A deftheory is never redundant. The ``natural'' notion of equivalent deftheorys is that the names and values of the two theory expressions are the same. But since most theory expressions are sensitive to the context in which they occur, it seems unlikely to us that two deftheorys coming from two sequentially included books will ever have the same values. So we prohibit redundant theory definitions. If you try to define the same theory name twice, you will get a ``name in use'' error.

An in-theory event is never redundant because it doesn't define any name.

A push-untouchable event is redundant if every name supplied is already a member of the untouchable symbols.

Table and defdoc events are never redundant because they don't define any name.

An encapsulate event is redundant if and only if a syntactically identical encapsulate has already been executed under the same default-defun-mode.

An include-book is redundant if the book has already been included.

Note About Shifting Logical Names:

Suppose a book defines a function fn and later uses fn as a logical name in a theory expression. Consider the value of that theory expression in two different sessions. In session A, the book is included in a world in which fn is not already defined, i.e., in a world in which the book's definition of fn is not redundant. In session B, the book is included in a world in which fn is already identically defined. In session B, the book's definition of fn is redundant. When fn is used as a logical name in a theory expression, it denotes the point in history at which fn was introduced. Observe that those points are different in the two sessions. Hence, it is likely that theory expressions involving fn will have different values in session A than in session B.

This may adversely affect the user of your book. For example, suppose your book creates a theory via deftheory that is advertised just to contain the names generated by the book. But suppose you compute the theory as the very last event in the book using:

(set-difference-theories (universal-theory :here) 
                         (universal-theory fn))

The moral of this is simple: when building books that other people will use, it is best to describe your theories in terms of logical names that will not shift around when the books are included. The best such names are those created by deflabel.

SAVING-AND-RESTORING

Major Section:  MISCELLANEOUS

Examples:
ACL2 !>:Q
>(make-lib "file")
...
>(note-lib "file")
>(LP)
ACL2 !>

To save the current ACL2 logical world to a file, exit ACL2 with :q and invoke (make-lib "file") in Common Lisp. This creates a file "file.lib" and a file "file.lisp". The latter will be compiled. It generally takes half an hour to save an ACL2 logical world and creates a 20Mb file. All things considered it is probably better to just save your core image.

To restore such a saved ACL2 world, invoke (note-lib "file") from Common Lisp, and then enter ACL2 with (lp). We do not save the io system, the stacks, or the global table, hence bindings of your globals will not be restored.

This save/restore mechanism is a temporary expedient. We know of faster mechanisms, mechanisms that consume less disk space, and mechanisms that provide more functionality. We don't know of good compromises between these various desirable features.

SIGNATURE

Major Section:  MISCELLANEOUS

Examples:
((hd *) => *)
((printer * state) => (mv * * state))
((mach * mach-state * state) => (mv * mach-state)


General Form:
((fn ...) => *)
((fn ...) => stobj)
or
((fn ...) => (mv ...))

where fn is the constrained function symbol, ... is a list of asterisks and/or the names of single-threaded objects and stobj is a single-threaded object name. ACL2 also supports an older style of signature described below after we describe the preferred style.

Signatures specify three syntactic aspects of a function symbol: (1) the ``arity'' or how many arguments the function takes, (2) the ``multiplicity'' or how many results it returns via MV, and (3) which of those arguments and results are single-threaded objects and which objects they are.

For a discussion of single-threaded objects, see stobj. For the current purposes it is sufficient to know that every single- threaded object has a unique symbolic name and that state is the name of the only built-in single-threaded object. All other stobjs are introduced by the user via defstobj. An object that is not a single-threaded object is said to be ``ordinary.''

The general form of a signature is ((fn x1 ... xn) => val). So a signature has two parts, separated by the symbol ``=>''. The first part, (fn x1 ... xn), is suggestive of a call of the constrained function. The number of ``arguments,'' n, indicates the arity of fn. Each xi must be a symbol. If a given xi is the symbol ``*'' then the corresponding argument must be ordinary. If a given xi is any other symbol, that symbol must be the name of a single-threaded object and the corresponding argument must be that object. No stobj name may occur twice among the xi.

The second part, val, of a signature is suggestive of a term and indicates the ``shape'' of the output of fn. If val is a symbol then it must be either the symbol ``*'' or the name of a single-threaded object. In either case, the multiplicity of fn is 1 and val indicates whether the result is ordinary or a stobj. Otherwise, val is of the form (mv y1 ... yk), where k > 1. Each yi must be either the symbol ``*'' or the name of a stobj. Such a val indicates that fn has multiplicity k and the yi indicate which results are ordinary and which are stobjs. No stobj name may occur twice among the yi.

Finally, a stobj name may appear in val only if appears among the xi.

Before ACL2 supported user-declared single-threaded objects there was only one single-threaded object: ACL2's built-in notion of state. The notion of signature supported then gave a special role to the symbol state and all other symbols were considered to denote ordinary objects. ACL2 still supports the old form of signature, but it is limited to functions that operate on ordinary objects or ordinary objects and state.

Old-Style General Form:
(fn formals result)

where fn is the constrained function symbol, formals is a suitable list of formal parameters for it, and result is either a symbol denoting that the function returns one result or else result is an mv expression, (mv s1 ... sn), where n>1, each si is a symbol, indicating that the function returns n results. At most one of the formals may be the symbol STATE, indicating that corresponding argument must be ACL2's built-in state. If state appears in formals then state may appear once in result. All ``variable symbols'' other than state in old style signatures denote ordinary objects, regardless of whether the symbol has been defined to be a single-threaded object name!

We also support a variation on old style signatures allowing the user to declare which symbols (besides state) are to be considered single-threaded object names. This form is

(fn formals result :stobjs names)

SIMPLE

Major Section:  MISCELLANEOUS

Example of simple rewrite rule:
(equal (car (cons x y)) x)


Examples of simple definition:
(defun file-clock-p (x) (integerp x))
(defun naturalp (x)
  (and (integerp x) (>= x 0)))

The theorem prover output sometimes refers to ``simple'' definitions and rewrite rules. These rules can be used by the preprocessor, which is one of the theorem prover's ``processes'' understood by the :do-not hint; see hints.

The preprocessor expands certain definitions and uses certain rewrite rules that it considers to be ``fast''. There are two ways to qualify as fast. One is to be an ``abbreviation'', where a rewrite rule with no hypotheses or loop stopper is an ``abbreviation'' if the right side contains no more variable occurrences than the left side, and the right side does not call the functions if, not or implies. Definitions and rewrite rules can both be abbreviations; the criterion for definitions is similar, except that the definition must not be recursive. The other way to qualify applies only to a non-recursive definition, and applies when its body is a disjunction or conjunction, according to a perhaps subtle criterion that is intended to avoid case splits.

SPECIOUS-SIMPLIFICATION

Major Section:  MISCELLANEOUS

Occasionally the ACL2 theorem prover reports that the current goal simplifies to itself or to a set including itself. Such simplifications are said to be ``specious'' and are ignored in the sense that the theorem prover acts as though no simplification were possible and tries the next available proof technique. Specious simplifications are almost always caused by forcing.

The simplification of a formula proceeds primarily by the local application of :rewrite, :type-prescription, and other rules to its various subterms. If no rewrite rules apply, the formula cannot be simplified and is passed to the next ACL2 proof technique, which is generally the elimination of destructors. The experienced ACL2 user pays special attention to such ``maximally simplified'' formulas; the presence of unexpected terms in them indicates the need for additional rules or the presence of some conflict that prevents existing rules from working harmoniously together.

However, consider the following interesting possibility: local rewrite rules apply but, when applied, reproduce the goal as one of its own subgoals. How can rewrite rules apply and reproduce the goal? Of course, one way is for one rule application to undo the effect of another, as when commutativity is applied twice in succession to the same term. Another kind of example is when rules conflict and undermine each other. For example, under suitable hypotheses, (length x) might be rewritten to (+ 1 (length (cdr x))) by the :definition of length and then a :rewrite rule might be used to ``fold'' that back to (length x). Generally speaking the presence of such ``looping'' rewrite rules causes ACL2's simplifier either to stop gracefully because of heuristics such as that described in the documentation for loop-stopper or to cause a stack overflow because of indefinite recursion.

A more insidious kind of loop can be imagined: two rewrites in different parts of the formula undo each other's effects ``at a distance,'' that is, without ever being applied to one another's output. For example, perhaps the first hypothesis of the formula is simplified to the second, but then the second is simplified to the first, so that the end result is a formula propositionally equivalent to the original one but with the two hypotheses commuted. This is thought to be impossible unless forcing or case-splitting occurs, but if those features are exploited (see force and see case-split) it can be made to happen relatively easily.

Here is a simple example. Declare foo to be a function of one argument returning one result:

(defstub foo (x) t)

(defaxiom forcer
 (implies (force (not (true-listp x)))
          (equal (foo x) t))
 :rule-classes :type-prescription)

(thm (implies (and (consp x)              ; hyp 1
                   (true-listp (cdr x))   ; hyp 2
                   (true-listp x))        ; hyp 3
              (foo x)))                   ; concl

(implies (and (consp x)                   ; rewritten hyp 1
              (true-listp (cdr x)))       ; rewritten hyp 3
         (foo x))                         ; unrewritten concl

(implies (and (consp x)                   ; rewritten hyp 1
              (true-listp (cdr x))        ; rewritten hyp 3
              (true-listp x))             ; FORCEd hyp
         (foo x)).                        ; unrewritten concl

If ACL2 were to adopt the new set of subgoals, it would loop indefinitely. Therefore, it checks whether the input goal is a member of the output subgoals. If so, it announces that the simplification is ``specious'' and pretends that no simplification occurred.

``Maximally simplified'' formulas that produce specious simplifications are maximally simplified in a very technical sense: were ACL2 to apply every applicable rule to them, no progress would be made. Since ACL2 can only apply every applicable rule, it cannot make further progress with the formula. But the informed user can perhaps identify some rule that should not be applied and make it inapplicable by disabling it, allowing the simplifier to apply all the others and thus make progress.

When specious simplifications are a problem it might be helpful to disable all forcing (including case-splits) and resubmit the formula to observe whether forcing is involved in the loop or not. See force. The commands

ACL2 !>:disable-forcing
and
ACL2 !>:enable-forcing

To illustrate what we mean by the claim that specious simplifications often arise because the system forces a false hypothesis, reconsider the example above. At the time we used the :type-prescription rule, the known assumptions were (consp x) and (true-listp (cdr x)). Observe that this tells us that x is a true list. But the hypothesis forced to be true was (not (true-listp x)). Why was the falsity of this hypothesis missed? The most immediate reason is that the encoding of the two assumptions above does not produce a context (``type-alist'') in which x is recorded to be a true-list. When we look up (not (true-listp x)) in that context, we are not told that it is false. More broadly, the problem stems from the fact that when we force a hypothesis we do not bring to bear on it all of the resources of the theorem prover. Thus it could be -- as here -- that the hypothesis could be proved false in the current context but is not obviously so. No matter how sophisticated we made the forcing mechanism, the unavoidable incompleteness of the theorem prover would still permit the occasional specious simplification. While that does not excuse us from trying to avoid specious simplifications when we can -- and we may well strengthen the type mechanism to deal with the problem illustrated here -- specious simplifications will probably remain a problem deserving of the user's attention.