EXECUTABLE-COUNTERPART

a rule for computing the value of a function
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.