Major Section: MISCELLANEOUS
Examples: (:executable-counterpart length)which may be abbreviated in theories as
(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.
