Executable-counterpart
A rule for computing the value of a function
This topic is about a type of rune that controls evaluation
using the executable-counterpart of a function. For discussion of
executable-counterparts of functions, see evaluation.
Example:
(:executable-counterpart length)
which may be abbreviated in theory expressions in either of the
following two ways (see rune).
(:e length)
(length)
Every defun introduces at least two rules used by the theorem
prover. Suppose fn is the name of a defun'd function. Then
(:definition fn) is the rune (see rune) naming the rule that
allows the simplifier to replace calls of fn by its instantiated body.
(:executable-counterpart fn) is the rune for the rule for how to
evaluate the function on known constants.
When typing theories it is convenient to know that (fn) is a
runic designator that denotes (:executable-counterpart fn). See theories.
If (:executable-counterpart fn) is enabled, then when
applications of fn to known constants are seen by the simplifier they are
computed out by executing the Common Lisp code for fn (with the
appropriate handling of guards). Suppose fact is defined as the
factorial function. If the executable-counterpart rune of fact,
(:executable-counterpart fact), is enabled when the simplifier
encounters (fact 12), then that term will be ``immediately'' expanded to
479001600. Note that even if subroutines of fn have disabled
executable-counterparts, fn will call their Lisp code nonetheless: once
an executable-counterpart function is applied, no subsidiary enable checks are
made.
Such one-step expansions are sometimes counterproductive because they
prevent the anticipated application of certain lemmas about the subroutines of
the expanded function. Such computed expansions can be prevented by disabling
the executable-counterpart rune of the relevant function. For example,
if (:executable-counterpart fact) is disabled, (fact 12) will
not be expanded by computation. In this situation, (fact 12) may be
rewritten to (* 12 (fact 11)), using the rule named (:definition
fact), provided the system's heuristics permit the introduction of the term
(fact 11). Note that lemmas about multiplication may then be applicable
(while such lemmas would be inapplicable to 479001600). In many proofs
it is desirable to disable the executable-counterpart runes of
certain functions to prevent their expansion by computation. See executable-counterpart-theory.
Finally: What do we do about functions that are ``constrained'' rather than
defined, such as the following? (See encapsulate.)
(encapsulate (((foo *) => *))
(local (defun foo (x) x)))
Does foo have an executable-counterpart? Yes: since the vast majority
of functions have sensible executable-counterparts, it was decided that
all functions, even such ``constrained'' ones, have
executable-counterparts. We essentially ``trap'' when such calls are
inappropriate. Thus, consider for example:
(defun bar (x)
(if (rationalp x)
(+ x 1)
(foo x)))
If the term (bar '3) is encountered by the ACL2 rewriter during a
proof, and if the :executable-counterpart of bar is enabled,
then it will be invoked to reduce this term to '4. However, if the term
(bar 'a) is encountered during a proof, then since 'a is not a
rationalp and since the :executable-counterpart of foo is
only a ``trap,'' then this call of the :executable-counterpart of
bar will result in a ``trap.'' In that case, the rewriter will return the
term (hide (bar 'a)) so that it never has to go through this process
again. See hide.
