FIND-RULES-OF-RUNE

Parent topic:  MISCELLANEOUS
Home

General Form:
(find-rules-of-rune rune wrld)

This function finds all the rules in wrld with :rune rune. It returns a list of rules in their internal form (generally as described by the corresponding defrec). Decyphering these rules is difficult since one cannot always look at a rule object and decide what kind of record it is without exploiting many system invariants (e.g., that :rewrite runes only name rewrite-rules).

At the moment this function returns nil if the rune in question is a :refinement rune, because there is no object representing :refinement rules. (:refinement rules cause changes in the 'coarsenings properties.) In addition, if the rune is an :equivalence rune, then congruence rules with that rune will be returned -- because :equivalence lemmas generate some congruence rules -- but the fact that a certain function is now known to be an equivalence relation is not represented by any rule object and so no such rule is returned. (The fact that the function is an equivalence relation is encoded entirely in its presence as a 'coarsening of equal.)

FORCE

Parent topic:  MISCELLANEOUS
Home

When a hypothesis of a conditional rule has the form (force hyp) it is logically equivalent to hyp but has a pragmatic effect. In particular, when the rule is considered, the needed instance of the hypothesis, hyp', is assumed and a special case is generated, requiring the system to prove that hyp' is true in the current context. The proofs of all such ``forced assumptions'' are delayed until the successful completion of the main goal. See forcing-round.

Forcing should only be used on hypotheses that are always expected to be true, such as the guards of functions. All the power of the theorem prover is brought to bear on a forced hypothesis and no backtracking is possible. If the :executable-counterpart of the function force is disabled, then no hypothesis is forced. See enable-forcing and see disable-forcing.

It sometimes happens that a conditional rule is not applied because some hypothesis, hyp, could not be relieved, even though the required instance of hyp, hyp', can be shown true in the context. This happens when insufficient resources are brought to bear on hyp' at the time we try to relieve it. A sometimes desirable alternative behavior is for the system to assume hyp', apply the rule, and to generate explicitly a special case to show that hyp' is true in the context. This is called ``forcing'' hyp. It can be arranged by restating the rule so that the offending hypothesis, hyp, is embedded in a call of force, as in (force hyp). By using the :corollary field of the rule-classes entry, a hypothesis can be forced without changing the statement of the theorem from which the rule is derived.

Technically, force is just a function of one argument that returns that argument. It is generally enabled and hence evaporates during simplification. But its presence among the hypotheses of a conditional rule causes case splitting to occur if the hypothesis cannot be conventionally relieved.

Since a forced hypothesis must be provable whenever the rule is otherwise applicable, forcing should be used only on hypotheses that are expected always to be true. A common situation is when the hypothesis is in fact a guard (or part of a guard) of some function involved in the pattern that triggers the rule. Intuitively, if that pattern term occurs in the current conjecture, then its guards had better be true, since otherwise nothing is known about the term.

A particularly common situation in which some hypotheses should be forced is in ``most general'' type-prescription lemmas. If a single lemma describes the ``expected'' type of a function, for all ``expected'' arguments, then it is probably a good idea to force the hypotheses of the lemma. Thus, every time a term involving the function arises, the term will be given the expected type and its arguments will be required to be of the expected type. In applying this advice it might be wise to avoid forcing those hypotheses that are in fact just type predicates on the arguments, since the routine that applies type-prescription lemmas has fairly thorough knowledge of the types of all terms.

Force can have the additional benefit of causing the ACL2 typing mechanism to interact with the ACL2 rewriter to establish the hypotheses of type-prescription rules. To understand this remark, think of the ACL2 type reasoning system as a rather primitive rule-based theorem prover for questions about Common Lisp types, e.g., ``does this expression produce a consp?'' ``does this expression produce some kind of ACL2 number, e.g., an integerp, a rationalp, or a complex-rationalp?'' etc. It is driven by type-prescription rules. To relieve the hypotheses of such rules, the type system recursively invokes itself. This can be done for any hypothesis, whether it is ``type-like'' or not, since any proposition, p, can be phrased as the type-like question ``does p produce an object of type nil?'' However, as you might expect, the type system is not very good at establishing hypotheses that are not type-like, unless they happen to be assumed explicitly in the context in which the question is posed, e.g., ``If p produces a consp then does p produce nil?'' If type reasoning alone is insufficient to prove some instance of a hypothesis, then the instance will not be proved by the type system and a type-prescription rule with that hypothesis will be inapplicable in that case. But by embedding such hypotheses in force expressions you can effectively cause the type system to ``punt'' them to the rest of the theorem prover. Of course, as already noted, this should only be done on hypotheses that are ``always true.'' In particular, if rewriting is required to establish some hypothesis of a type-prescription rule, then the rule will be found inapplicable because the hypothesis will not be established by type reasoning alone.

The ACL2 rewriter uses the type reasoning system as a subsystem. It is therefore possible that the type system will force a hypothesis that the rewriter could establish. Before a forced hypothesis is reported out of the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A type-prescription rule fails to apply because some true hypothesis is not being relieved. The user changes the rule so as to force the hypothesis. The system then applies the rule but reports no forcing. How can this happen? The type system ``punted'' the forced hypothesis to the rewriter, which established it.

Finally, we should mention that the rewriter is never willing to force when there is an if term present in the goal being simplified. Since and and or terms are merely abbreviations for if terms, they also prevent forcing.

FORCING-ROUND

Parent topic:  MISCELLANEOUS
Home

If ACL2 ``forces'' some hypothesis of some rule to be true, it is obliged later to prove the hypothesis. See force. ACL2 delays the consideration of forced hypotheses until the main goal has been proved. It then undertakes a new round of proofs in which the main goal is essentially the conjunction of all hypotheses forced in the preceding proof. Call this round of proofs the ``Forcing Round.'' Additional hypotheses may be forced by the proofs in the Forcing Round. The attempt to prove these hypotheses is delayed until the Forcing Round has been successfully completed. Then a new Forcing Round is undertaken to prove the recently forced hypotheses and this continues until no hypotheses are forced. Thus, there is a succession of Forcing Rounds.

The Forcing Rounds are enumerated starting from 1. The Goals and Subgoals of a Forcing Round are printed with the round's number displayed in square brackets. Thus, "[1]Subgoal 1.3" means that the goal in question is Subgoal 1.3 of the 1st forcing round. To supply a hint for use in the proof of that subgoal, you should use the goal specifier "[1]Subgoal 1.3". See goal-spec.

When a round is successfully completed -- and for these purposes you may think of the proof of the main goal as being the 0th forcing round -- the system collects all of the assumptions forced by the just-completed round. Here, an assumption should be thought of as an implication, (implies context hyp), where context describes the context in which hyp was assumed true. Before undertaking the proofs of these assumptions, we try to ``clean them up'' in an effort to reduce the amount of work required. This is often possible because the forced assumptions are generated by the same rule being applied repeatedly in a given context.

For example, suppose the main goal is about some term (pred (xtrans i) i) and that some rule rewriting pred contains a forced hypothesis that the first argument is a good-inputp. Suppose that during the proof of Subgoal 14 of the main goal, (good-inputp (xtrans i)) is forced in a context in which i is an integerp and x is a consp. (Note that x is irrelevant.) Suppose finally that during the proof of Subgoal 28, (good-inputp (xtrans i)) is forced ``again,'' but this time in a context in which i is a rationalp and x is a symbolp. Since the forced hypothesis does not mention x, we deem the contextual information about x to be irrelevant and discard it from both contexts. We are then left with two forced assumptions: (implies (integerp i) (good-inputp (xtrans i))) from Subgoal 14, and (implies (rationalp i) (good-inputp (xtrans i))) from Subgoal 28. Note that if we can prove the assumption required by Subgoal 28 we can easily get that for Subgoal 14, since the context of Subgoal 28 is the more general. Thus, in the next forcing round we will attempt to prove just

(implies (rationalp i) (good-inputp (xtrans i)))

By delaying and collecting the forced assumptions until the completion of the ``main goal'' we gain two advantages. First, the user gets confirmation that the ``gist'' of the proof is complete and that all that remains are ``technical details.'' Second, by delaying the proofs of the forced assumptions ACL2 can undertake the proof of each assumption only once, no matter how many times it was forced in the main goal.

In order to indicate which proof steps of the previous round were responsible for which forced assumptions, we print a sentence explaining the origins of each newly forced goal. For example,

[1]Subgoal 1, below, will focus on
(GOOD-INPUTP (XTRANS I)),
which was forced in
 Subgoal 14, above,
  by applying (:REWRITE PRED-CRUNCHER) to
  (PRED (XTRANS I) I),
 and
 Subgoal 28, above,
  by applying (:REWRITE PRED-CRUNCHER) to
  (PRED (XTRANS I) I).

In this entry, ``[1]Subgoal 1'' is the name of a goal which will be proved in the next forcing round. On the next line we display the forced hypothesis, call it x, which is (good-inputp (xtrans i)) in this example. This term will be the conclusion of the new subgoal. Since the new subgoal will be printed in its entirety when its proof is undertaken, we do not here exhibit the context in which x was forced. The sentence then lists (possibly a succession of) a goal name from the just-completed round and some step in the proof of that goal that forced x. In the example above we see that Subgoals 14 and 28 of the just-completed proof forced (good-inputp (xtrans i)) by applying (:rewrite pred-cruncher) to the term (pred (xtrans i) i).

If one were to inspect the theorem prover's description of the proof steps applied to Subgoals 14 and 28 one would find the word ``forced'' (or sometimes ``forcibly'') occurring in the commentary. Whenever you see that word in the output, you know you will get a subsequent forcing round to deal with the hypotheses forced. Similarly, if at the beginning of a forcing round a rune is blamed for causing a force in some subgoal, inspection of the commentary for that subgoal will reveal the word ``forced'' after the rule name blamed.

Most forced hypotheses come from within the prover's simplifier. When the simplifier encounters a hypothesis of the form (force hyp) it first attempts to establish it by rewriting hyp to, say, hyp'. If the truth or falsity of hyp' is known, forcing is not required. Otherwise, the simplifier actually forces hyp'. That is, the x mentioned above is hyp', not hyp, when the forced subgoal was generated by the simplifier.

Once the system has printed out the origins of the newly forced goals, it proceeds to the next forcing round, where those goals are individually displayed and attacked.

At the beginning of a forcing round, the enabled structure defaults to the global enabled structure. For example, suppose some rune, rune, is globally enabled. Suppose in some event you disable the rune at "Goal" and successfully prove the goal but force "[1]Goal". Then during the proof of "[1]Goal", rune is enabled ``again.'' The right way to think about this is that the rune is ``still'' enabled. That is, it is enabled globally and each forcing round resumes with the global enabled structure.

GENERALIZED-BOOLEANS

Parent topic:  MISCELLANEOUS
Home

The discussion below outlines a potential source of unsoundness in ACL2. Although to our knowledge there is no existing Lisp implementation in which this problem can arise, nevertheless we feel compelled to explain this situation.

Consider for example the question: What is the value of (equal 3 3)? According to the ACL2 axioms, it's t. And as far as we know, based on considerable testing, the value is t in every Common Lisp implementation. However, according the Common Lisp draft proposed ANSI standard, any non-nil value could result. Thus for example, (equal 3 3) is allowed by the standard to be 17.

The Common Lisp standard specifies (or soon will) that a number of Common Lisp functions that one might expect to return Boolean values may, in fact, return arbitrary values. Examples of such functions are equal, rationalp, and <; a much more complete list is given below. Indeed, we dare to say that every Common Lisp function that one may believe returns only Booleans is, nevertheless, not specified by the standard to have that property, with the exceptions of the functions not and null. The standard refers to such arbitrary values as ``generalized Booleans,'' but in fact this terminology makes no restriction on those values. Rather, it merely specifies that they are to be viewed, in an informal sense, as being either nil or not nil.

This situation is problematic for ACL2, which axiomatizes these functions to return Booleans. The problem is that because (for efficiency and simplicity) ACL2 makes very direct use of compiled Common Lisp functions to support the execution of its functions, there is in principle a potential for unsoundness due to these ``generalized Booleans.'' For example, ACL2's equal function is defined to be Common Lisp's equal. Hence if in Common Lisp the form (equal 3 3) were to evaluate to 17, then in ACL2 we could prove (using the :executable-counterpart of equal) (equal (equal 3 3) 17). However, ACL2 can also prove (equal (equal x x) t), and these two terms together are contradictory, since they imply (instantiating x in the second term by 3) that (equal 3 3) is both equal to 17 and to t.

To make matters worse, the standard allows (equal 3 3) to evaluate to different non-nil values every time. That is: equal need not even be a function!

Fortunately, no existing Lisp implementation takes advantage of the flexibility to have (most of) its predicates return generalized Booleans, as far as we know. We may implement appropriate safeguards in future releases of ACL2, in analogy to (indeed, probably extending) the existing safeguards by way of guards (see guard). For now, we'll sleep a bit better knowing that we have been up-front about this potential problem.

The following list of functions contains all those that are defined in Common Lisp to return generalized Booleans but are assumed by ACL2 to return Booleans. In addition, the functions acl2-numberp and complex-rationalp are directly defined in terms of respective Common Lisp functions numberp and complexp.

/=
<
=
alpha-char-p
atom
char-equal
char<
char<=
char>
char>=
characterp
consp
digit-char-p
endp
eq
eql
equal
evenp
integerp
keywordp
listp
logbitp
logtest
lower-case-p
minusp
oddp
plusp
rationalp
standard-char-p
string-equal
string<
string<=
string>
string>=
stringp
subsetp
symbolp
upper-case-p
zerop

GOAL-SPEC

Parent topic:  MISCELLANEOUS
Home

Examples:
"Goal"
"goal"
"Subgoal *1/3''"
"subgoal *1/3''"
"[2]Subgoal *1/3''"

When hints are given to the theorem prover, a goal-spec is provided to specify the goal to which the hints are to be applied. The hints provided are carried along innocuously until the named goal arises. When it arises, the hints are ``activated'' for that goal and its descendents.

A legal goal specification may be extracted from the theorem prover's output. Certain lines clearly label formulas, as in

Subgoal *1/3.2'
(IMPLIES ... ...)

[1]Subgoal *1/3.2'
(IMPLIES ... ...).

"[1]Subgoal *1/3.2'"

As noted, a hint is applied to a goal when the hint's goal specification matches the name ACL2 assigns to the goal. The matching algorithm is case-insensitive. Thus, alternative goal specifications for the goal above are "[1]subgoal *1/3.2'" and "[1]SUBGOAL *1/3.2'". The matching algorithm does not tolerate non-case discrepancies. Thus, "[1]Subgoal*1/3.2'" and " [1]Subgoal *1/3.2'" are unacceptable.

Sometimes a formula is given two names, e.g.,

Subgoal *1/14.2'
(IMPLIES ... 
         ...)
Name the formula above *1.1.

("Subgoal *1/14.2'" :use ...)

But what if you want to give an :induct hint? By the time induction is tried, the formula has been given the name *1.1. Well, this is one you just have to remember:

("Subgoal *1/14.2'" :induct ...).

GUARD

Parent topic:  MISCELLANEOUS
Home

The ACL2 system provides a mechanism for restricting a function definition to a particular domain. Although such restrictions, which are called ``guards,'' are actually ignored by the ACL2 logic, they can be useful as a specification device or as a means of causing the execution of definitions directly in Common Lisp. To make such a restriction, use the :guard xarg to defun. See xargs for a discussion of how to use :guard. The general issue of guards and guard verification is discussed in the topics listed below.

• GUARD-INTRODUCTION -- introduction to guards in ACL2

• GUARD-MISCELLANY -- miscellaneous remarks about guards

• GUARD-QUICK-REFERENCE -- brief summary of guard checking and guard verification

• GUARDS-AND-EVALUATION -- the relationship between guards and evaluation

• GUARDS-FOR-SPECIFICATION -- guards as a specification device

• GUARD-EXAMPLE -- a brief transcript illustrating guards in ACL2

• SET-GUARD-CHECKING -- control checking guards during execution of top-level forms

• SET-VERIFY-GUARDS-EAGERNESS -- the eagerness with which guard verification is tried.

• VERIFY-GUARDS -- verify the guards of a function

GUARD-INTRODUCTION

Parent topic:  GUARD
Home

Most users can probably profit by avoiding dealing with guards most of the time. If they seem to get in the way, they can be ``turned off'' using the command :set-guard-checking nil; for more about this, see set-guard-checking. For more about guards in general, see guard.

The guard on a function symbol is a formula about the formals of the function. To see the guard on a function, use the keyword command :args. See args. To specify the guard on a function at defun-time, use the :guard xarg. See xargs.

Guards can be seen as having either of two roles: (a) they are a specification device allowing you to characterize the kinds of inputs a function ``should'' have, or (b) they are an efficiency device allowing logically defined functions to be executed directly in Common Lisp. Briefly: If the guards of a function definition are ``verified'' (see verify-guards), then the evaluation of a call of that function on arguments satisfying its guard will have the following property:

All subsequent function calls during that evaluation will be on arguments satisfying the guard of the called function.

Let us turn next to the issue of the relationship between guards and evaluation. See guards-and-evaluation.

GUARD-MISCELLANY

Parent topic:  GUARD
Home

The discussion of guards concludes here with a few miscellaneous remarks. (Presumably you found this documentation by following a link; see guards-for-specification.) For further information related to guards other than what you find under ``guard,'' see any of the following documentation topics: guard-example, set-verify-guards-eagerness, set-guard-checking, and verify-guards.

Defun can be made to try to verify the guards on a function. This is controlled by the ``defun-mode'' of the defun; see defun-mode. The defun-mode is either as specified with the :mode xarg of the defun or else defaults to the default defun-mode. See default-defun-mode. If the defun-mode of the defun is :logic and either a :guard is specified or :verify-guards t is specified in the xargs, then we attempt to verify the guards of the function. Otherwise we do not.

It is sometimes impossible for the system to verify the guards of a recursive function at definition time. For example, the guard conjectures might require the invention and proof of some inductively derived property of the function (as often happens when the value of a recursive call is fed to a guarded subroutine). So sometimes it is necessary to define the function using :verify-guards nil then to state and prove key theorems about the function, and only then have the system attempt guard verification. Post-defun guard verification is achieved via the event verify-guards. See verify-guards.

It should be emphasized that guard verification affects only two things: how fast ACL2 can evaluate the function and whether the function is executed correctly by raw Common Lisp, without guard violations. Since ACL2 does not use the raw Common Lisp definition of a function to evaluate its calls unless that function's guards have been verified, the latter effect is felt only if you run functions in raw Common Lisp rather than via ACL2's command loop.

Guard verification does not otherwise affect the theorem prover or the semantics of a definition. If you are not planning on running your function on ``big'' inputs and you don't care if your function runs correctly in raw Common Lisp (e.g., you have formalized some abstract mathematical property and just happened to use ACL2 as your language), there is no need to suffer through guard verification. Often users start by not doing guard verification and address that problem later. Sometimes you are driven to it, even in mathematical projects, because you find that you want to run your functions particularly fast or in raw Common Lisp.

If certify-book is used to compile a file, and the file contains functions with unverified guard conjectures, then you will be warned that the compiled file cannot be loaded into raw Common Lisp with the expectation that the functions will run correctly. This is just the same point we have been making: ACL2 and Common Lisp agree only on the restricted domains specified by our guards. When guards are violated, Common Lisp can do anything. When you call a compiled function on arguments violating its guards, the chances are only increased that Common Lisp will go berserk, because compiled functions generally check fewer things at runtime and tend to be more fragile than interpreted ones.

GUARD-QUICK-REFERENCE

Parent topic:  GUARD
Home

For a careful introduction to guards, see guard.

I. GUARD CHECKING DURING EXECUTION

Effect

Guards on definitions are checked at execution time (except for guards on subsidiary calls of recursive or mutually recursive functions).

When does it happen

By default, guards are checked for all forms submitted at the top level.

To disable
:set-guard-checking nil

To (re-)enable
:set-guard-checking t

II. GUARD VERIFICATION

Effect

A proof is attempted of the obligations arising from the guards of subsidiary functions in a defun, defthm, or defaxiom event.

When does it happen

Only names of defined functions, defthms, and defaxioms are subject to guard verification. Guard verification may occur when functions are defined (using defun), but it requires an explicit call of verify-guards in order to verify guards for defthms and defaxioms. Constrained functions (see encapsulate) may not have their guards verified.

(verify-guards foo ...)
causes guard verification for the defun, defthm, or defaxiom named by foo, if it has not already been successfully done. The default defun-mode (see default-defun-mode) must be :logic, or else this event is ignored.

(defun foo ...)
causes guard verification of foo if and only if the following conditions are both met. (However, see set-verify-guards-eagerness for how to change this behavior.)

1. Foo is processed in :logic mode (either by setting mode :logic globally, or by including :mode :logic in the xargs declaration).

2. The xargs declaration (see xargs) either specifies :guard or specifies :verify-guards t (or both).

(verify-termination foo ...)
causes guard verification of foo if foo is a function currently defined in :program mode and the appropriate xargs are supplied, as discussed for the case of defun above. The default defun-mode (see default-defun-mode) must be :logic, or else this event is ignored.

GUARDS-AND-EVALUATION

Parent topic:  GUARD
Home

The guard has no effect on the logical axiom added by the definition of a function. It does, however, have consequences for how calls of that function are evaluated in ACL2. We begin by explaining those consequences, when ACL2 is in its default ``mode,'' i.e., as originally brought up. In subsequent discussion we'll consider other ways that guards can interact with evaluation. For more about guards in general, see guard. Also see generalized-booleans for discussion about a subtle issue in the evaluation of certain Common Lisp functions.

Guards and evaluation I: the default

Consider the following very simple definition.

(defun foo (x) (cons 1 (cdr x)))

Now by default, ACL2 evaluates calls of foo exactly as Common Lisp does, except that it uses guards to check the ``legality'' of each function call. So for example, since (cdr x) has a guard of (or (consp x) (equal x nil)), the call (foo 7) would cause a ``guard violation,'' as illustrated below.

ACL2 !>(foo 7)


ACL2 Error in TOP-LEVEL:  The guard for the function symbol CDR, which
is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
call (CDR 7).


ACL2 !>

Guards and evaluation II: :set-guard-checking.

The ACL2 logic is a logic of total functions. That is, every application of a function defined has a completely specified result. See the documentation for each individual primitive for the specification of what it returns when its guard is violated; for example, see cdr.

The presence of guards thus introduces a choice in the sense of evaluation. When you type a form for evaluation do you mean for guards to be checked or not? Put another way, do you mean for the form to be evaluated in Common Lisp (if possible) or in the ACL2 logic? Note: If Common Lisp delivers an answer, it will be the same as in the logic, but it might be erroneous to execute the form in Common Lisp. For example, the ACL2 logic definition of cdr implies that the cdr of an atom is nil; see cdr. So: should (cdr 7) cause a guard violation error or return nil?

The top-level ACL2 loop has a variable which controls which sense of execution is provided. By default, ``guard checking'' is on, by which we mean that guards are checked at runtime, in the sense already described. To turn it off, do :set-guard-checking nil. To turn ``guard checking'' back on, execute the top-level form :set-guard-checking t. The status of this variable is reflected in the prompt; guard-checking is ``on'' when the prompt contains an exclamation mark (also see default-print-prompt). For example,

ACL2 !>

ACL2 > 

ACL2 !>(car 'abc)

ACL2 >(car 'abc)

Guards and evaluation III: guard verification

Consider the defininition of foo given above, but modified so that a reasonable guard of (consp x) is specified, as shown below.

(defun foo (x)
  (declare (xargs :guard (consp x)))
  (cons 1 (cdr x)))

The verify-guards event has been provided for this purpose. Details may be found elsewhere; see verify-guards. Briefly, for any defined function fn, the event (verify-guards fn) attempts to check the condition discussed above, that whenever fn is called on arguments that satisfy its guard, the evaluation of this call will proceed without any guard violation. If this check is successful, then future calls of this sort will be evaluated in raw Common Lisp.

Returning to our example above, the (verify-guards foo) will succeed because the guard (consp x) of foo implies the guard generated from the call (cdr x) in the body of the definition, namely, (or (consp x) (equal x nil)) (see cdr). Then the evaluation of (foo (cons 'a 3)) will take place in raw Common Lisp, because (cons 'a 3) satisfies the guard of foo.

This ability to dive into raw Common Lisp hinges on the proof that the guards you attach to your own functions are sufficient to insure that the guards encountered in the body are satisfied. This is called ``guard verification.'' Once a function has had its guards verified, then ACL2 can evaluate the function somewhat faster (but see ``Guards and evaluation V: efficiency issues'' below). Perhaps more importantly, ACL2 can also guarantee that the function will be evaluated correctly by any implementation of Common Lisp (provided the guard of the function is satisfied on the input). That is, if you have verified the guards of a system of functions and you have determined that they work as you wish in your host ACL2 (perhaps by proving it, perhaps by testing), then they will work identically in any Common Lisp.

There is a subtlety to our treatment of evaluation of calls of functions whose guards have been verified. If the function's guard is not satisfied by such a call, then no further attempt is made to evaluate any call of that function in raw lisp during the course of evaluation of that call. This is obvious if guard checking is on, because an error is signalled the first time its guard is violated; but in fact it is also true when guard checking is off. See guard-example for an example.

Guards and evaluation IV: functions having :program mode

Strictly speaking, functions in :program mode (see defun-mode) do not have definitions in the ACL2 logic. So what does it mean to evaluate calls of such functions in ACL2? Our decision is to treat :program functions exactly as we treat :logic functions whose guards have been verified, except that when there is a guard violation we signal an error regardless of whether guard checking is currently on or off. Note that when the guard of a function in :logic mode is violated, there is still a value that the ACL2 logic proves is equal to the given call. But the same cannot be said for a function in :program mode, so we really have no choice but to signal an error when there is a guard violation for such a function.

To summarize: as with :logic functions, when a guard has been satisfied on a call of a function with :program mode, no subsidiary guard checking will be done.

Consider the same example foo as above, but where foo is submitted in :program mode. Then even with guard checking off, top-level calls of foo will signal a guard violation when the arguments do not satisfy the guard of foo, e.g., (foo 7).

Notice that by treating functions in :program mode like functions whose guards have been verified, we are using raw lisp to compute their values when their guards are met. We do not check guards any further once raw lisp is invoked. This can lead to hard lisp errors if the guards are not appropriate, as illustrated below.

ACL2 >:program
ACL2 p>(defun foo (x)
        (declare (xargs :guard t))
        (cons 1 (cdr x)))


Summary
Form:  ( DEFUN FOO ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.02)
 FOO
ACL2 p>(foo 3)


Error: 3 is not of type LIST.
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by CDR.
Broken at COND.  Type :H for Help.
ACL2>>

Guards and evaluation V: efficiency issues

We have seen that by verifying the guards for a :logic function, we arrange that raw lisp is used for evaluation of calls of such functions when the arguments satisfy its guard.

This has several apparent advantages over the checking of guards as we go. First, the savings is magnified as your system of functions gets deeper: the guard is checked upon the top-level entry to your system and then raw Common Lisp does all the computing. Second, if the raw Common Lisp is compiled, enormous speed-ups are possible. Third, if your Common Lisp or its compiler does such optimizations as tail-recursion removal, raw Common Lisp may be able to compute your functions on input much ``bigger'' than ACL2 can.

The first of these advantages is quite important if you have complicated guards. However, the other two advantages are probably not very important, as we now explain.

When a function is defined in :logic mode, its defun is executed in raw Common Lisp. (We might call this the ``primary'' raw lisp definition of the function.) However, a corresponding ``logic definition'' is also executed. The ``logic definition'' is a defun in raw lisp that checks guards at runtime and escapes to the primary raw lisp definition if the guard holds of the arguments and the function has already had its guards verified. Otherwise the logic definition executes the body of the function by calling the logic definitions of each subroutine. Now it is true that compilation generally speeds up execution enormously. However, the :comp command (see comp) compiles both of the raw lisp definitions associated with a :logic function. Also, we have attempted to arrange that for every tail recursion removal done on the actual defun, a corresonding tail recursion removal is done on the ``logic definition.''

We believe that in most cases, the logic definition executes almost as fast as the primary raw lisp definition, at least if the evaluation of the guards is fast. So, the main advantage of guard verification is probably that it lets you know that the function may be executed safely in raw lisp, returning the value predicted by the ACL2 logic, whenever its arguments satisfy its guard. We envision the development of systems of applicative lisp functions that have been developed and reasoned about using ACL2 but which are intended for evaluation in raw Common Lisp (perhaps with only a small ``core'' of ACL2 loaded), so this advantage of guard verification is important.

Nevertheless, guard verification might be important for optimal efficiency when the functions make use of type declarations. For example, at this writing, the GCL implementation of Common Lisp can often take great advantage of declare forms that assign small integer types to formal parameters.

To continue the discussion of guards, see guards-for-specification to read about the use of guards as a specification device.

GUARDS-FOR-SPECIFICATION

Parent topic:  GUARD
Home

A use of guard verification that has nothing to do with efficiency is as a way to gain confidence in specifications. This use has the feel of ``types'' in many traditional programming languages, though guards allow much greater expressiveness than most systems of types (and unfortunately, as a result they are not syntactically checkable).

For more discussion of guards in general, see guard.

Suppose you have written a collection of function definitions that are intended to specify the behavior of some system. Perhaps certain functions are only intended to be called on certain sorts of inputs, so you attach guards to those functions in order to ``enforce'' that requirement. And then, you verify the guards for all those functions.

Then what have you gained, other than somewhat increased efficiency of execution (as explained above), which quite possibly isn't your main concern? You have gained the confidence that when evaluating any call of a (specification) function whose arguments satisfy that function's guard, all subsequent function calls during the course of evaluation will have this same property, that the arguments satisfy the guard of the calling function. In logical terms, we can say that the equality of the original call with the returned value is provable from weakened versions of the definitions, where each definitional axiom is replaced by an implication whose antecedent is the requirement that the arguments satisfy the guard and whose consequent is the original axiom. For example,

(defun foo (x)
  (declare (xargs :guard (consp x)))
  (cons 1 (cdr x)))

(equal (foo x)
       (cons 1 (cdr x)))

(implies (consp x)
         (equal (foo x)
                (cons 1 (cdr x))))