Warrant
Giving apply$ permission to handle a user-defined function in proofs
The word ``warrant'' is defined in the Merriam-Webster dictionary
as ``a commission or document giving authority to do something....''
The discussion below mentions the concept of badges, which are
easily confused with warrants. See the discussion of Badges versus
Warrants at the top of defbadge. But roughly put, badges extend
the ACL2 syntax and warrants extend the proof theory. You'll need a badge
for fn to allow the system to syntactically analyze (apply$ 'fn
...). You'll need a both a badge and a warrant for fn if you wish to
reason about that term with ACL2. Badges and warrants also have impact on
evaluation of forms in the top-level loop. See guarantees-of-the-top-level-loop.
In the ACL2 proof theory, the functions badge and apply$
are undefined on user-defined function symbols. To be precise, when
presented with a user-defined function symbol, badge calls the weakly
constrained function badge-userfn and apply$ calls the weakly
constrained function apply$-userfn. Warrants are terms that, if
available as hypotheses in a conjecture, further constrain those functions
for specific function symbols. If there is a warrant for fn among the
hypotheses of a conjecture, (badge 'fn) and (apply$ 'fn ...) can
be simplified appropriately. In particular, (badge 'fn) is simplified
to the actual badge of fn and (apply$ 'fn ...) is simplified to the
appropriate application of fn provided the arguments are suitably tame. We think of the warrant for fn giving badge and apply$
authority to expand on 'fn. For reasons of logical consistency not
every fn can have a warrant. Warrants are issued, when possible, by
defwarrant.
In the ACL2 evaluation theory — a consistent extension of the proof
theory — all warrants issued by defwarrant are implicitly assumed,
meaning badge and apply$ can be executed on warranted user-defined
function symbols at the top-level of the ACL2 loop without explicit mention
of the warrants. In fact, just as the evaluation theory can —
``magically'' — execute :program mode functions despite the
absence of any axioms about them, the evaluation theory can execute a
well-formed apply$ on any :program mode function that has a badge. However, for a :logic mode function fn, the top-level loop
cannot evaluate (apply$ 'fn ...) unless (defwarrant fn) has
previously succeeded. See guarantees-of-the-top-level-loop.) For a
discussion of the restrictions on when a fn can be warranted, see defwarrant. This topic discusses warrants per se, their names, their
logical meaning, when they must be explicitly added as hypotheses to
conjectures, and their consistency.
Logical Definition of the Warrant of a Function
If fn has a warrant, then the warrant is the term
(apply$-warrant-fn), i.e., a call of the 0-ary
warrant function named, apply$-warrant-fn. That warrant
function name is admitted to the logic when defwarrant succeeds on
fn.
The warrant function for fn, introduced by (defwarrant fn), is
defined with defun-sk because the warrant must specify the values
returned by (apply$ 'fn args) for all possible args.
Recall that badge and apply$ defer to two undefined
functions, badge-userfn and apply$-userfn, when they are applied to
user-defined function symbols. The warrant for fn is actually phrased
in terms of those two undefined functions. By stipulating their values on
'fn the warrant determines the values of (badge 'fn) and (apply$
'fn ...). To create the warrant function for fn, defwarrant
must turn the ilks of fn into tameness requirements on the corresponding
elements of the args to which fn will be applied by apply$.
Each :FN argument must be a tame function and each :EXPR
argument must be a tame expression.
It is easiest to understand the above paragraph by looking at the
generated warrant function for foldr, whose definition is shown at the
top of the documentation for apply$ and whose badge is
(APPLY$-BADGE 3 1 NIL :FN NIL), indicating that foldr takes 3
arguments of ilks NIL, :FN, and NIL, and returns 1 result.
The warrant function for foldr is defined as follows.
(defun-sk apply$-warrant-foldr ()
(forall (args)
(implies (tamep-functionp (cadr args))
(and (equal (badge-userfn 'FOLDR)
'(APPLY$-BADGE 3 1 NIL :FN NIL))
(equal (apply$-userfn 'FOLDR args)
(foldr (car args)
(cadr args)
(caddr args))))))
:constrain t)
Notice also that the tameness hypothesis involves the universally
quantified variable args, but that the first conjunct of the conclusion
does not mention that variable. So we can read (apply$-warrant-foldr)
as equivalent to the conjunction of:
(equal (badge-userfn 'FOLDR)
'(APPLY$-BADGE 3 1 NIL :FN NIL))
and
(forall (args)
(implies (tamep-functionp (cadr args))
(equal (apply$-userfn 'FOLDR args)
(foldr (car args)
(cadr args)
(caddr args)))))
The first specifies the value of the undefined function used by badge
to find the badge of a user-defined function. The second specifies the
behavior of the undefined function used by apply$ to apply$
'FOLDR and requires that the second element of args be a tame function.
Finally, notice that the warrant function for foldr,
apply$-warrant-foldr, ancestrally depends on foldr: foldr is
called in the defun-sk. That is crucial to avoiding the LOCAL
problem noted in introduction-to-apply$. If the warrant for
foldr is required for a theorem's proof (which it will be if the proof
involves ``expanding'' (apply$ 'FOLDR ...)), then the theorem is
ancestrally dependent on foldr even though that function symbol may not
be otherwise mentioned in the theorem. That, in turn, means that foldr
may not be a locally defined symbol in the environment from which the theorem
is exported.
Now consider a function symbol that returns more than one result. Suppose
the badge of add-and-subtract is (APPLY$-BADGE 2 2 . T), meaning it
takes two ordinary objects and returns two results. The function is tame and
so no tameness requirements are imposed on its application. Its warrant is
defined
(defun-sk apply$-warrant-add-and-subtract ()
(forall (args)
(and (equal (badge-userfn 'add-and-subtract)
'(APPLY$-BADGE 2 2 . T))
(equal (apply$ 'add-and-subtract args)
(mv-list 2
(add-and-subtract (car args) (cadr args)))))))
Rewrite Rules that Lift and Force the Warrant
Once defwarrant has introduced the warrant function for fn it
proves two rewrite rules, conjoined under the name apply$-fn,
that ``lifts'' the warrant from the level of the two undefined functions to
the level of badge and apply$. In the case of foldr the rules
are:
(defthm apply$-foldr
(and (implies (force (apply$-warrant-foldr))
(equal (badge 'FOLDR)
'(APPLY$-BADGE 3 1 NIL :FN NIL)))
(implies (and (force (apply$-warrant-foldr))
(tamep-functionp (car (cdr args))))
(equal (apply$ 'FOLDR args)
(foldr (car args)
(car (cdr args))
(car (cdr (cdr args))))))))
Observe that these rules say that if (apply$-warrant-foldr) is
available as a hypothesis, then (badge 'FOLDR) is (APPLY$-BADGE 3 1
NIL :FN NIL) and (apply$ 'FOLDR args) has the naively expected
behavior of calling foldr, provided the second element of args is a
tamep-functionp. Also note that the warrant hypothesis is forced in both rules.
The effect of these rules is if either (badge 'FOLDR) or any instance
of (apply$ 'FOLDR args) arises during a proof, the warrant for
foldr is raised and either relieved or forced. The badge and
apply$ terms are simplified whether the warrant is present or not, but
if the warrant is not among the hypotheses and the proof is otherwise
successful, the warrant for foldr will show up in a checkpoint.
If no warrant has been issued for foldr these terms will not
simplify.
Determining the Necessary Warrants
There is no easy way to determine the warrants you'll need to make a
formula a theorem. At first this seems to be a problem that could be solved
with a few rules of thumb and indeed, there are a few useful rules. But they
don't guarantee success.
Rule 1. One way to determine sufficient warrants for a formula to
be a theorem is to attempt to prove the formula without warrants and see the
checkpoints. This may have to be repeated to collect sufficient warrants and
can be frustrating. Furthermore, as illustrated further below, it can lead
to unnecessary warrants.
Most users attempt to anticipate what warrants are needed.
Rule 2. You will probably need a warrant hypothesis for every
user-defined function symbol mentioned in the fully translated term occupying
any slot of ilk :FN in the formula you're trying to prove. The two
common situations are quoted user-defined function symbols in such slots and
lambda$ expressions. In the latter case, you must consider every
user-defined function symbol in the fully translated body of the
lambda$ expression. (If you've ignored our recommendations to use
lambda$ instead of hand-typed quoted LAMBDA objects, you'll have to
look at those too.)
But Rule 2 says ``probably need a warrant'' because whether you do or not
depends on what you're proving. In the examples below, suppose we have
carried out these events.
(include-book "projects/apply/top" :dir :system)
(defun$ sq (x) (* x x))
and recall that collect$ is loop$ scion logically defined
as
(defun$ collect$ (fn lst)
(if (endp lst)
nil
(cons (apply$ fn (list (car lst)))
(collect$ fn (cdr lst)))))
No warrant is really needed to prove
(thm (equal (collect$ 'sq (append a b))
(append (collect$ 'sq a) (collect$ 'sq b))))
because it could be proved by appealing to the more general
(thm (equal (collect$ fn (append a b))
(append (collect$ fn a)
(collect$ fn b))))
which makes clear that the properties of sq are totally irrelevant to
the proof of this formula.
But if you followed Rule 1 and just submitted
(thm (equal (collect$ 'sq (append a b))
(append (collect$ 'sq a)
(collect$ 'sq b))))
the proof would fail with a checkpoint indicating that you need the
warrant for sq. That happens because the :rewrite rules proved by
defwarrant, discussed in the previous section and named apply$-sq
in the case of sq, fire and force that warrant. However, you could
disable that rule and get the proof without a warrant.
To further dim our hopes for a simple way to identify warrants,
consider
(defun$ square (i) (apply$ 'sq (list i)))
and then the proof of
(thm (equal (square i) (* i i)))
This theorem requires the warrant for sq even though 'sq is not
mentioned in the top-level statement of the theorem. The problem, of course,
is that the mention of 'sq in a :FN slot is mentioned in the
definition of square.
Rule 3. You may need warrants for any symbols used in :FN
slots in the definitions of any function appearing in the formula.
And then of course there is the usual reason you need forgotten
hypotheses: some lemma critical to your proof has that hypothesis.
For example, one could imagine proving
(defthm lemma
(implies (apply$-warrant-sq)
(equal (square x) (sq x))))
and then try to prove
(thm (equal (square x) (* x x))
:hints (("Goal" :in-theory (disable square))))
hoping the lemma would reduce (square x) to (sq x) and then
(sq x) would expand to (* x x). But of course, the lemma isn't
applicable because we can't establish its hypothesis. The point here is that
another source of required warrants can be the warrant hypotheses of any
lemmas needed for the proof. We could posit a ``Rule 4'' but what's the
point?
Returning to the first thing we said in this section, there is no easy
sure-fire way to determine the warrants you'll need. It just depends on the
functions you're manipulating, the cases explored in the proof, the
hypotheses of crucial lemmas, etc. However, our experience is that it's not
nearly so hard as we're suggesting here!
Basically you'll need a warrant for fn if the proof requires
apply$ to behave as naively expected on 'fn or the warrant is
required for some lemma. Chances are you'll know when you're depending on
the meaning of a quoted symbol and when you're not. And Rule 1 will
eventually get you there though it may generate unnecessary warrant
hypotheses.
There is another piece of good news perhaps best explained by example.
Imagine that you've defined and warranted your own versions of the
familiar list concatenation and list reverse functions under the names
ap and rv.
(defun$ ap (x y)
(if (endp x)
y
(cons (car x)
(ap (cdr x) y))))
(defun$ rv (x)
(if (endp x)
nil
(ap (rv (cdr x))
(list (car x)))))
What warrant(s) do you need to prove
(implies (true-listp x)
(equal (apply$ 'rv (list (apply$ 'rv (list x)))) x))?
You clearly need the warrant for rv. But do you need the warrant for
its subfunction ap? Some users fall into the trap of thinking they do.
They think they'll need warrants for all the subfunctions of any function
requiring a warrant. We fall into this trap when we think all
evaluation is carried out by ev$ and apply$. Put another way,
if we defined
(defun$ rv1 (x)
(if (endp x)
nil
(apply$ 'ap
(list (rv1 (cdr x))
(list (car x))))))
and then tried to prove
(implies (true-listp x)
(equal (apply$ 'rv1 (list (apply$ 'rv1 (list x)))) x))
we would indeed need warrants for both rv1 and ap, as per Rule
3, because rv1 apply$s 'ap.
But the warrant for the original rv says that (apply$ 'rv args)
is (unconditionally) equal to (rv (car args)). There are no
apply$s left in the problem once we get to a call of the ACL2 function
rv. We don't need any warrants, even to evaluate a function we called
via apply$ unless the definition of the function itself involves further
apply$s.
A Convenient Macro for Conjoining Warrants
Because ``APPLY$-WARRANT-fn'' is hard to remember, we
provide a macro for referring to the conjunction of warrant terms for a list
of functions.
General Form:
(warrant fn1 fn2 ... fnk)
where each fni is the name of a defined function on which
defwarrant has been previously called and succeeded. (Actually, we
allow the fni to include certain primitive function symbols already
built into apply$, but for the moment we ignore the possible presence of
such symbols among the arguments to warrant.) (Warrant fn1 fn2
... fnk) expands to:
(AND (FORCE (APPLY$-WARRANT-fn1))
(FORCE (APPLY$-WARRANT-fn2))
...
(FORCE (APPLY$-WARRANT-fnk)))
Because there are over 800 ACL2 primitives built into apply$, it can
be hard to look at a conjecture involving, say, a lambda$ term, and
list all and only the function names that need warrants. For example, if the
body of the lambda$ term calls logeqv it will expand into
binary-logeqv and the diligent user might anticipate, accurately, that
the ev$ of that body will involve (apply$ 'BINARY-LOGEQV ...) and
thus might suppose that binary-logeqv be included among the fni
listed in the warrant hypothesis. But no warrant for binary-logeqv
exists, that is, apply$-warrant-binary-logeqv is not defined, because
binary-logeqv is built into apply$. For this reason, we do not
insist that every fni in warrant's argument be a function
possessing a warrant. Instead, the warrant macro ignores those fni
built into apply$. It does cause an error if one of the fni has no
warrant and is not built in.
The (warrant fn1 fn2 ... fnk) macro forces the warrants
because (a) we assume the only use of the macro is to add warrant hypotheses
to conjectures and (b) by forcing warrants aggressively the prover ``almost
completes'' more proofs and enters a forcing round that highlights the need
to assume those warrants. When a rewrite rule, for example, is conditioned
on a warrant that is not forced (as would happen if you added the hyps
(apply$-warrant-fn1), (apply$-warrant-fn2), etc.), then the rule
will not fire if a subsequent conjecture omitted the warrants. Of course,
this raises the question ``But are all the warrants really true?''
Why Warrants Don't Render Theorems Vacuous
Adding warrants to formulas certainly restricts (weakens) the resulting
theorem since it is only applicable when the warrant is assumed. But an
important question to ponder is whether adding warrants can actually make a
formula vacuously valid? That is, can a set of warrants simply be
unsatisfiable so that any formula having that set of warrants among its
hypotheses is a theorem? Put another way, is there a model for the set of
all warrants introduced by defwarrant?
The answer is yes. This is discussed in ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore. For any set of functions warranted by defwarrant
it is possible to define, under the standard ACL2 definitional
principle, versions of those functions (together with apply$, ev$,
etc.) and then make attachments to the undefined badge-userfn and
apply$-userfn, and so that every warrant is provably equal to T.
In fact, the resultant theory is the basis of ACL2's evaluation theory where
all warranted functions can be apply$d (under the appropriate tameness
requirements) without explicit mention of warrants. The crux of the proof is
admitting a big mutually recursive clique containing versions of apply$
and all of its scions, by inventing a measure that provably decreases
as apply$ and the scions call each other. The keys to that measure's
existence are the restrictions imposed by defwarrant and tameness. See the paper for a sketch of the proof and see the comment
titled Essay on Admitting a Model for Apply$ and the Functions that Use
It in the ACL2 source file apply-raw.lisp.
