LD-SKIP-PROOFSP

Major Section:  MISCELLANEOUS

Examples:
ACL2 !>(set-ld-skip-proofsp t state)
 T
ACL2 !s>(set-ld-skip-proofsp nil state)
 NIL
ACL2 !>(set-ld-skip-proofsp 'include-book state)
 INCLUDE-BOOK
ACL2 !s>

A global variable in the ACL2 state, called 'ld-skip-proofsp, determines the thoroughness with which ACL2 processes your commands. This variable may take on one of three values: t, nil or 'include-book. When ld-skip-proofsp is non-nil, the system assumes that which ought to be proved and is thus unsound. The form (set-ld-skip-proofsp flg state) is the general-purpose way of setting ld-skip-proofsp. This global variable is an ``ld special,'' which is to say, you may call ld in such a way as to ``bind'' this variable for the dynamic extent of the ld.

When ld-skip-proofsp is non-nil, the default prompt displays the character s. Thus, the prompt

ACL2 !s>

Observe that there are two legal non-nil values, t and 'include-book. When ld-skip-proofsp is t, ACL2 skips all proof obligations but otherwise performs all other required analysis of input events. When ld-skip-proofsp is 'include-book, ACL2 skips not only proof obligations but all analysis except that required to compute the effect of successfully executed events. To explain the distinction, let us consider one particular event, say a defun. Very roughly speaking, a defun event normally involves a check of the syntactic well-formedness of the submitted definition, the generation and proof of the termination conditions, and the computation and storage of various rules such as a :definition rule and some :type-prescription rules. By ``normally'' above we mean when ld-skip-proofsp is nil. How does a defun behave when ld-skip-proofsp is non-nil?

If ld-skip-proofsp is t, then defun performs the syntactic well-formedness checks and computes and stores the various rules, but it does not actually carry out the termination proofs. If ld-skip-proofsp is 'include-book, defun does not do the syntactic well-formedness check nor does it carry out the termination proof. Instead, it merely computes and stores the rules under the assumption that the checks and proofs would all succeed. Observe that a setting of 'include-book is ``stronger'' than a setting of t in the sense that 'include-book causes defun to assume even more about the admissibility of the event than t does.

As one might infer from the choice of name, the include-book event sets ld-skip-proofsp to 'include-book when processing the events in a book being loaded. Thus, include-book does the miminal work necessary to carry out the effects of every event in the book. The syntactic checks and proof obligations were, presumably, successfully carried out when the book was certified.

A non-nil value for ld-skip-proofsp also affects the system's output messages. Event summaries (the paragraphs that begin ``Summary'' and display the event forms, rules used, etc.) are not printed when ld-skip-proofsp is non-nil. Warnings and observations are printed when ld-skip-proofsp is t but are not printed when it is 'include-book.

Intuitively, ld-skip-proofsp t means skip just the proofs and otherwise do all the work normally required for an event; while ld-skip-proofsp 'include-book is ``stronger'' and means do as little as possible to process events. In accordance with this intuition, local events are processed when ld-skip-proofsp is t but are skipped when ld-skip-proofsp is 'include-book.

The ACL2 system itself uses only two settings, nil and 'include-book, the latter being used only when executing the events inside of a book being included. The ld-skip-proofsp setting of t is provided as a convenience to the user. For example, suppose one has a file of events. By loading it with ld with ld-skip-proofsp set to t, the events can all be checked for syntactic correctness and assumed without proof. This is a convenient way to recover a state lost by a system crash or to experiment with a modification of an events file.

The foregoing discussion is actually based on a lie. ld-skip-proofsp is allowed two other values, 'initialize-acl2 and 'include-book-with-locals. The first causes behavior similar to t but skips local events and avoids some error checks that would otherwise prevent ACL2 from properly booting. The second is identical to 'include-book but also executes local events. These additional values are not intended for use by the user, but no barriers to their use have been erected.

We close by reminding the user that ACL2 is potentially unsound if ld-skip-proofsp is ever set by the user. We provide access to it simply to allow experimentation and rapid reconstruction of lost or modified logical worlds.

LD-VERBOSE

Major Section:  MISCELLANEOUS

Ld-verbose is an ld special (see ld). The accessor is (ld-verbose state) and the updater is (set-ld-verbose val state). Ld-verbose must be t, nil or a string or consp suitable for fmt printing via the ~@ command. The initial value of ld-verbose is a fmt message that prints the ACL2 version number, ld level and connected book directory.

Before processing the forms in standard-oi, ld may print a header. The printing of this header is controlled by ld-verbose. If ld-verbose is nil, no header is printed. If it is t, ld prints the message

   ACL2 loading <file>

LEMMA-INSTANCE

Major Section:  MISCELLANEOUS

Lemma instances are the objects one provides via :use and :by hints (see hints) to bring to the theorem prover's attention some previously proved or easily provable fact. A typical use of the :use hint is given below. The value specified is a list of five lemma instances.

:use (reverse-reverse
      (:type-prescription app)
      (:instance assoc-of-app
                 (x a) (y b) (z c))
      (:functional-instance p-f
                            (p consp) (f flatten))
      (:instance (:theorem (equal x x))
                 (x (flatten a))))

:use reverse-reverse

:use (:instance assoc-of-app (x a) (y b) (z c))

A lemma instance denotes a formula which is either known to be a theorem or which must be proved to be a theorem before it can be used. To use a lemma instance in a particular subgoal, the theorem prover adds the formula as a hypothesis to the subgoal before the normal theorem proving heuristics are applied.

A lemma instance, or lmi, is of one of the following five forms:

(1) name, where name names a previously proved theorem, axiom, or definition and denotes the formula (theorem) of that name.

(2) rune, where rune is a rune (see rune) denoting the :corollary justifying the rule named by the rune.

(3) (:theorem term), where term is any term alleged to be a theorem. Such a lemma instance denotes the formula term. But before using such a lemma instance the system will undertake to prove term.

(4) (:instance lmi (v1 t1) ... (vn tn)), where lmi is recursively a lemma instance, the vi's are distinct variables and the ti's are terms. Such a lemma instance denotes the formula obtained by instantiating the formula denoted by lmi, replacing each vi by ti.

(5) (:functional-instance lmi (f1 g1) ... (fn gn)), where lmi is recursively a lemma instance and each fi is an ``instantiable'' function symbol of arity ni and gi is a function symbol or a pseudo-lambda expression of arity ni. An instantiable function symbol is any defined or constrained function symbol except the primitives not, member, implies, and e0-ord-<, and a few others, as listed by the constant *non-instantiable-primitives*. These are built-in in such a way that we cannot recover the constraints on them. A pseudo-lambda expression is an expression of the form (lambda (v1 ... vn) body) where the vi are distinct variable symbols and body is any term. No a priori relation is imposed between the vi and the variables of body, i.e., body may ignore some vi's and may contain ``free'' variables. However, we do not permit v to occur freely in body if the functional substitution is to be applied to any formula (lmi or the constraints to be satisfied) that contains v as a variable. This is our draconian restriction to avoid capture. If you happen to violate this restriction by choosing a v that does occur, say in one of the relevant constraints, an informative error message will be printed. That message will list for you the illegal choices for v in the context in which the functional substitution is offered. A :functional-substitution lemma instance denotes the formula obtained by functionally instantiating the formula denoted by lmi, replacing fi by gi. However, before such a lemma instance can be used, the system will undertake to prove that the gi's satisfy the constraints (see constraint) on the fi's. Any such constraint that was generated and proved by ACL2 on behalf of a previously-proved event will be considered proved.

LOCAL-INCOMPATIBILITY

Major Section:  MISCELLANEOUS

Sometimes a ``local incompatibility'' is reported while attempting to embed some events, as in an encapsulate or include-book. This is generally due to the use of a locally defined name in a non-local event or the failure to make a witnessing definition local.

Local incompatibilities may be detected while trying to execute the strictly non-local events of an embedding. For example, encapsulate operates by first executing all the events (local and non-local) with ld-skip-proofsp nil, to confirm that they are all admissible. Then it attempts merely to assume the non-local ones to create the desired theory, by executing the events with ld-skip-proofsp set to 'include-book. Similarly, include-book assumes the non-local ones, with the understanding that a previously successful certify-book has performed the admissiblity check.

How can a sequence of events admitted with ld-skip-proofsp nil fail when ld-skip-proofsp is 'include-book? The key observation is that in the latter case only the non-local events are processed. The local ones are skipped and so the non-local ones must not depend upon them.

Two typical mistakes are suggested by the detection of a local incompatibility: (1) a locally defined function or macro was used in a non-local event (and, in the case of encapsulate, was not included among the signatures) and (2) the witnessing definition of a function that was included among the signatures of an encapsulate was not made local.

An example of mistake (1) would be to include among your encapsulated events both (local (defun fn ...)) and (defthm lemma (implies (fn ...) ...)). Observe that fn is defined locally but a formula involving fn is defined non-locally. In this case, either the defthm should be made local or the defun should be made non-local.

An example of mistake (2) would be to include (fn (x) t) among your signatures and then to write (defun fn (x) ...) in your events, instead of (local (defun fn ...)).

One subtle aspect of encapsulate is that if you constrain any member of a mutually recursive clique you must define the entire clique locally and then you must constrain those members of it you want axiomatized non-locally.

Errors due to local incompatibility should never occur in the assumption of a fully certified book. Certification insures against it. Therefore, if include-book reports an incompatibility, we assert that earlier in the processing of the include-book a warning was printed advising you that some book was uncertified. If this is not the case -- if include-book reports an incompatibility and there has been no prior warning about lack of certification -- please report it to us.

When a local incompatibility is detected, we roll-back to the world in which we started the encapsulate or include-book. That is, we discard the intermediate world created by trying to process the events skipping proofs. This is clean, but we realize it is very frustrating because the entire sequence of events must be processed from scratch. Assuming that the embedded events were, once upon a time, processed as top-level commands (after all, at some point you managed to create this sequence of commands so that the local and non-local ones together could survive a pass in which proofs were done), it stands to reason that we could define a predicate that would determine then, before you attempted to embed them, if local incompatibilities exist. We hope to do that, eventually.

LOGICAL-NAME

Major Section:  MISCELLANEOUS

Examples:
assoc
caddr
+
"ACL2-USER"
"arith"
"project/task-1/arith.lisp"
:here

A logical name is either a name introduced by some event, such as defun, defthm, or include-book, or else is the keyword :here, which refers to the most recent such event. See events. Every logical name is either a symbol or a string. For the syntactic rules on names, see name. The symbols name functions, macros, constants, axioms, theorems, labels, and theories. The strings name packages or books. We permit the keyword symbol :here to be used as a logical name denoting the most recently completed event.

The logical name introduced by an include-book is the full book name string for the book (see full-book-name). Thus, under the appropriate setting for the current book directory (see cbd) the event (include-book "arith") may introduce the logical name

"/usr/home/smith/project/task-1/arith.lisp" .

"/local/src/acl2/library/arith.lisp" .

A logical name that is a string is either a package name or a book name. If it is not a package name, we support various conventions to interpret it as a book name. If it does not end with the string ".lisp" we extend it appropriately. Then, we search for any book name that has the given logical name as a terminal substring. Suppose (include-book "arith") is the only include-book so far and that "/usr/home/smith/project/task-1/arith.lisp" is the source file it processed. Then "arith", "arith.lisp" and "task-1/arith.lisp" are all logical names identifying that include-book event (unless they are package names). Now suppose a second (include-book "arith") is executed and processes "/local/src/acl2/library/arith.lisp". Then "arith" is no longer a logical name, because it is ambiguous. However, "task-1/arith" is a logical name for the first include-book and "library/arith" is a logical name for the second. Indeed, the first can be named by "1/arith" and the second by "y/arith".

Logical names are used primarily in the theory manipulation functions, e.g., universal-theory and current-theory with which you may obtain some standard theories as of some point in the historical past. The reference points are the introductions of logical names, i.e., the past is determined by the events it contains. One might ask, ``Why not discuss the past with the much more flexible language of command descriptors?'' (See command-descriptor.) The reason is that inside of such events as encapsulate or macro commands that expand to progns of events, command descriptors provide too coarse a grain.

When logical names are used as referents in theory expressions used in books, one must consider the possibility that the defining event within the book in question becomes redundant by the definition of the name prior to the assumption of the book. See redundant-events.

LOOP-STOPPER

Major Section:  MISCELLANEOUS

See rule-classes for a discussion of the syntax of the :loop-stopper field of :rewrite rule-classes. Here we describe how that field is used, and also how that field is created when the user does not explicitly supply it.

For example, the built-in :rewrite rule commutativity-of-+,

(implies (and (acl2-numberp x)
              (acl2-numberp y))
         (equal (+ x y) (+ y x))),

Our explanation of loop-stopping is in four parts. First we discuss ACL2's notion of ``term order.'' Next, we bring in the notion of ``invisibility'', and use it together with term order to define orderings on terms that are used in the loop-stopping algorithm. Third, we describe that algorithm. These topics all assume that we have in hand the :loop-stopper field of a given rewrite rule; the fourth and final topic describes how that field is calculated when it is not supplied by the user.

ACL2 must sometimes decide which of two terms is syntactically simpler. It uses a total ordering on terms, called the ``term order.'' Under this ordering constants such as '(a b c) are simpler than terms containing variables such as x and (+ 1 x). Terms containing variables are ordered according to how many occurrences of variables there are. Thus x and (+ 1 x) are both simpler than (cons x x) and (+ x y). If variable counts do not decide the order, then the number of function applications are tried. Thus (cons x x) is simpler than (+ x (+ 1 y)) because the latter has one more function application. Finally, if the number of function applications do not decide the order, a lexicographic ordering on Lisp objects is used. See term-order for details.

When the loop-stopping algorithm is controlling the use of permutative :rewrite rules it allows term1 to be moved leftward over term2 only if term1 is smaller, in a suitable sense. Note: The sense used in loop-stopping is not the above explained term order but a more complicated ordering described below. The use of a total ordering stops rules like commutativity from looping indefinitely because it allows (+ b a) to be permuted to (+ a b) but not vice versa, assuming a is smaller than b in the ordering. Given a set of permutative rules that allows arbitrary permutations of the tips of a tree of function calls, this will normalize the tree so that the smallest argument is leftmost and the arguments ascend in the order toward the right. Thus, for example, if the same argument appears twice in the tree, as x does in the binary-+ tree denoted by the term (+ a x b x), then when the allowed permutations are done, all occurrences of the duplicated argument in the tree will be adjacent, e.g., the tree above will be normalized to (+ a b x x).

Suppose the loop-stopping algorithm used term order, as noted above, and consider the binary-+ tree denoted by (+ x y (- x)). The arguments here are in ascending term order already. Thus, no permutative rules are applied. But because we are inside a +-expression it is very convenient if x and (- x) could be given virtually the same position in the ordering so that y is not allowed to separate them. This would allow such rules as (+ i (- i) j) = j to be applied. In support of this, the ordering used in the control of permutative rules allows certain unary functions, e.g., the unary minus function above, to be ``invisible'' with respect to certain ``surrounding'' functions, e.g., + function above.

Briefly, a unary function symbol fn1 is invisible with respect to a function symbol fn2 if fn2 belongs to the value of fn1 in invisible-fns-alist; also see set-invisible-fns-alist, which explains its format and how it can be set by the user. Roughly speaking, ``invisible'' function symbols are ignored for the purposes of the term-order test.

Consider the example above, (+ x y (- x)). The translated version of this term is (binary-+ x (binary-+ y (unary-- x))). The initial invisible-fns-alist makes unary-- invisible with repect to binary-+. The commutativity rule for binary-+ will attempt to swap y and (unary-- x) and the loop-stopping algorithm is called to approve or disapprove. If term order is used, the swap will be disapproved. But term order is not used. While the loop-stopping algorithm is permuting arguments inside a binary-+ expression, unary-- is invisible. Thus, insted of comparing y with (unary-- x), the loop-stopping algorithm compares y with x, approving the swap because x comes before y.

Here is a more precise specification of the total order used for loop-stopping with respect to a list, fns, of functions that are to be considered invisible. Let x and y be distinct terms; we specify when ``x is smaller than y with respect to fns.'' If x is the application of a unary function symbol that belongs to fns, replace x by its argument. Repeat this process until the result is not the application of such a function; let us call the result x-guts. Similarly obtain y-guts from y. Now if x-guts is the same term as y-guts, then x is smaller than y in this order iff x is smaller than y in the standard term order. On the other hand, if x-guts is different than y-guts, then x is smaller than y in this order iff x-guts is smaller than y-guts in the standard term order.

Now we may describe the loop-stopping algorithm. Consider a rewrite rule with conclusion (equiv lhs rhs) that applies to a term x in a given context; see rewrite. Suppose that this rewrite rule has a loop-stopper field (technically, the :heuristic-info field) of ((x1 y1 . fns-1) ... (xn yn . fns-n)). (Note that this field can be observed by using the command :pr with the name of the rule; see pr.) We describe when rewriting is permitted. The simplest case is when the loop-stopper list is nil (i.e., n is 0); in that case, rewriting is permitted. Otherwise, for each i from 1 to n let xi' be the actual term corresponding to the variable xi when lhs is matched against the term to be rewritten, and similarly correspond yi' with y. If xi' and yi' are the same term for all i, then rewriting is not permitted. Otherwise, let k be the least i such that xi' and yi' are distinct. Let fns be the list of all functions that are invisible with respect to every function in fns-k, if fns-k is non-empty; otherwise, let fns be nil. Then rewriting is permitted if and only if yi' is smaller than xi' with respect to fns, in the sense defined in the preceding paragraph.

It remains only to describe how the loop-stopper field is calculated for a rewrite rule when this field is not supplied by the user. (On the other hand, to see how the user may specify the :loop-stopper, see rule-classes.) Suppose the conclusion of the rule is of the form (equiv lhs rhs). First of all, if rhs is not an instance of the left hand side by a substitution whose range is a list of distinct variables, then the loop-stopper field is nil. Otherwise, consider all pairs (u . v) from this substitution with the property that the first occurrence of v appears in front of the first occurrence of u in the print representation of rhs. For each such u and v, form a list fns of all functions fn in lhs with the property that u or v (or both) appears as a top-level argument of a subterm of lhs with function symbol fn. Then the loop-stopper for this rewrite rule is a list of all lists (u v . fns).

LP

Major Section:  MISCELLANEOUS

To enter the ACL2 command loop from Common Lisp, call the Common Lisp program lp (which stands for ``loop,'' as in ``read-eval-print loop'' or ``command loop.'') The ACL2 command loop is actually coded in ACL2 as the function ld (which stands for ``load''). The command loop is just what you get by loading from the standard object input channel, *standard-oi*. Calling ld directly from Common Lisp is possible but fragile because hard lisp errors or aborts throw you out of ld and back to the top-level of Common Lisp. Lp calls ld in such a way as to prevent this and is thus the standard way to get into the ACL2 command loop. Also see acl2-customization for information on the loading of an initialization file.

All of the visible functionality of lp is in fact provided by ld, which is written in ACL2 itself. Therefore, you should see ld for detailed documentation of the ACL2 command loop. We sketch it below, for novice users.

Every expression typed to the ACL2 top-level must be an ACL2 expression.

Any ACL2 expression may be submitted for evaluation. Well-formedness is checked. Some well-formed expressions cannot be evaluated because they involve (at some level) undefined constrained functions (see encapsulate). In addition, ACL2 does not allow ``global variables'' in expressions to be evaluated. Thus, (car '(a b c)) is legal and evaluates to A, but (car x) is not, because there is no ``global context'' or binding environment that gives meaning to the variable symbol x.

There is an exception to the global variable rule outlined above: single-threaded objects (see stobj) may be used as global variables in top-level expressions. The most commonly used such object is the ACL2 ``current state,'' which is the value of the variable symbol state. This variable may occur in the top-level form to be evaluated, but must be passed only to ACL2 functions ``expecting'' state as described in the documentation for state and for stobjs in general. If the form returns a new state object as one of its values, then that is considered the new ``current'' state for the evaluation of the subsequent form. See state.

ACL2 provides some support for the functionality usually provided by global variables in a read-eval-print loop, namely the saving of the result of a computation for subsequent re-use in another expression. See assign and see @.

If the form read is a single keyword, e.g., :pe or :ubt, then special procedures are followed. See keyword-commands.

The command loop keeps track of the commands you have typed and allows you to review them, display them, and roll the logical state back to that created by any command. See history.

ACL2 makes the convention that if a top-level form returns three values, the last of which is an ACL2 state, then the first is treated as a flag that means ``an error occurred,'' the second is the value to be printed if no error occurred, and the third is (of course) the new state. When ``an error occurs'' no value is printed. Thus, if you execute a top-level form that happens to return three such values, only the second will be printed (and that will only happen if the first is nil!). See ld for details.

MACRO-ARGS

Major Section:  MISCELLANEOUS

Examples:
(x y z)
(x y z &optional max (base '10 basep))
(x y &rest rst)
(x y &key max base)
(&whole sexpr x y)

The ``lambda-list'' of a macro definition may include simple formal parameter names as well as appropriate uses of the following lambda-list keywords from CLTL (pp. 60 and 145), respecting the order shown:

  &whole,
  &optional,
  &rest,
  &body,
  &key, and
  &allow-other-keys.

(1) initialization forms in &optional and &key specifiers must be quoted values;

(2) &allow-other-keys may only be used once, as the last specifier; and

(3) destructuring is not allowed.

(defmacro demo (x y &optional opt &key key1 key2)
  (list 'quote (list x y opt key1 key2)))

  term                         value
(demo 1 2)                (1 2 NIL NIL NIL)
(demo 1 2 3)              (1 2 3 NIL NIL)
(demo 1 2 :key1 3)        error:  non-even key/value arglist
                          (because :key1 is used as opt)
(demo 1 2 3 :key2 5)      (1 2 3 NIL 5)

NAME

Major Section:  MISCELLANEOUS

Examples                 Counter-Examples


PRIMEP               91         (not a symbolp)
F-AC-23              :CHK-LIST  (in KEYWORD package)
1AX                  *PACKAGE*  (in the Lisp Package)
|Prime Number|       1E3        (not a symbolp)

Many different ACL2 entities have names, e.g., functions, macros, variables, constants, packages, theorems, theories, etc. Package names are strings. All other names are symbols and may not be in the "KEYWORD" package. Moreover, names of functions, macros, constrained functions, and constants, other than those that are predefined, must not be in the ``main Lisp package'' (which is ("LISP" or "COMMON-LISP", according to whether we are following CLTL1 or CLTL2). An analogous restriction on variables is given below.

T, nil, and all names above except those that begin with ampersand (&) are names of variables or constants. T, nil, and those names beginning and ending with star (*) are constants. All other such names are variables.

Note that names that start with ampersand, such as &rest, may be lambda list keywords and are reserved for such use whether or not they are in the CLTL constant lambda-list-keywords. (See pg 82 of CLTL2.) That is, these may not be used as variables. Unlike constants, variables may be in the main Lisp package as long as they are in the original list of imports from that package to ACL2, the list *common-lisp-symbols-from-main-lisp-package*, and do not belong to a list of symbols that are potentially ``global.'' This latter list is the value of *common-lisp-specials-and-constants*.

Our restrictions pertaining to the main Lisp package take into account that some symbols, e.g., lambda-list-keywords and boole-c2, are ``special.'' Permitting them to be bound could have harmful effects. In addition, the Common Lisp language does not allow certain manipulations with many symbols of that package. So, we stay away from them, except for allowing certain variables as indicated above.

OBDD

Major Section:  MISCELLANEOUS

See bdd for information on this topic.

OTF-FLG

Major Section:  MISCELLANEOUS

The value of this flag is normally nil. If you want to prevent the theorem prover from abandoning its initial work upon pushing the second subgoal, set :otf-flg to t.

Suppose you submit a conjecture to the theorem prover and the system splits it up into many subgoals. Any subgoal not proved by other methods is eventually set aside for an attempted induction proof. But upon setting aside the second such subgoal, the system chickens out and decides that rather than prove n>1 subgoals inductively, it will abandon its initial work and attempt induction on the originally submitted conjecture. The :otf-flg (Onward Thru the Fog) allows you to override this chickening out. When :otf-flg is t, the system will push all the initial subgoals and proceed to try to prove each, independently, by induction.

Even when you don't expect induction to be used or to succeed, setting the :otf-flg is a good way to force the system to generate and display all the initial subgoals.

The :otf-flg may be supplied to defun via the xargs declare option. When you supply an :otf-flg hint to defun, the flag is effective for the termination proofs and the guard proofs, if any.