Defun-mode-lambdas
:program mode functions in lambda objects
A rough rule-of-thumb is that all functions mentioned in a
:logic mode defun must themselves be in :logic
mode. If prgm is a :program mode function then (defun
fn (x) (prgm x)) is illegal. But there are situations (always involving
apply$) in which :program mode function symbols are allowed to
be mentioned in :logic mode defuns. We explain here.
Here are two example terms that mention the badged (see defbadge)
:program mode symbol prgm.
(apply$ (lambda$ (e) (prgm e)) (list x))
(loop$ for e in lst collect (prgm e))
Are such terms permitted in the defun of a :logic mode function?
The answer is complicated because it depends on whether the defun is
loop$ recursive and whether the defun will also try to verify
the guards of fn.
First, a :logic mode function may apply$ a quoted :program
mode symbol, whether guards are being verified or not. For example,
(apply$ 'prgm args) is legal. Here prgm is just a quoted symbol.
Since prgm is a :program mode symbol, there are no axioms about it,
so during proofs such a call of apply$ is not evaluated or expanded. If
this form is evaluated at the top-level -- where :program mode functions
are evaluable -- apply$ checks the guards of prgm just as it would
before any :program mode function is called.
The situation is more complicated for use of :program mode functions
in forms like lambda$, well-formed quoted lambda objects, and
loop$. The reason is that in guard-verified code, these forms are
generally executed via compiled code and that requires that the loop$
and lambda objects be Common Lisp compliant, which in turn implies they
must be analyzable by the prover. Since formally loop$s are understood
as calls of scions on lambda$ expressions it suffices for us to
discuss the lambda$ case alone. Well-formed quoted LAMBDA objects
are treated the same way.
So again, suppose you're defining a :logic mode function fn.
Suppose fn is not loop$ recursive and guards are not being verified
during the defun. Then badged :program mode symbols may be used
lambda$ forms in the definition of fn.
If fn is loop$ recursive, i.e., :loop$-recursion
t is declared, then all symbols used as functions in lambda$ forms
must be in :logic mode. The reason is that the measure conjectures
generated must be in :logic mode to be provable.
If fn is to be guard-verified, then all symbols used as functions in
lambda$ forms must be in :logic mode. The reason is that the guard
conjectures must be in :logic mode to be provable.
When a :program function is permitted in a :logic mode definition
the system will print a warning to alert you to the possibility that proofs
will fail. For example, the following events are legal
(include-book "projects/apply/top" :dir :system)
(defun prgm (x)
(declare (xargs :mode :program))
(list 'hi x))
(defbadge prgm)
(defun fn1 (x)
(declare (xargs :mode :logic))
(apply$ 'prgm (list x)))
but the last event will print:
ACL2 Warning [Problematic-quoted-fns] in ( DEFUN FN1 ...): The definition of
FN1 is in :LOGIC mode but mentions the :PROGRAM mode function HELLO in one or
more :FN or :EXPR slots. Conjectures about FN1 may not be provable until
this program is converted to :LOGIC mode and warranted! See :DOC
verify-termination and defwarrant.
Uses of prgm in quoted well-formed LAMBDA objects, lambda$
forms, and loop$ forms will cause similar warning messages to be
printed.
