Lambda$
Lambda object constructor for use with apply$
Lambda$ is a built-in ACL2 ``macro'' that allows you to enter
well-formed fully-translated quoted LAMBDA objects in argument positions
of ilk :FN. We urge you to use lambda$ instead of trying to type
quoted LAMBDA objects meant for use by apply$. We explain and
document lambda$ below.
Intuitively, a quoted LAMBDA object is a quoted constant like
'(LAMBDA (X) (BINARY-+ '1 X))
e.g., a quoted constant beginning with the symbol LAMBDA and listing
some formal variables, possibly some declarations, and a fully translated
body satisfying various rules. Apply$ can handle quoted LAMBDA
objects provided they have the right basic shape and all the listed formals
are symbols and the bodies are tame. But it is difficult to type
fully translated bodies and, for runtime efficiency, it is important that the
quoted LAMBDA objects satisfy additional (logically unnecessary)
well-formedness restrictions allowing faster guard checking and
compilation.
One should strive to always enter ``well-formed LAMBDA objects.''
The details of well-formedness may be found in well-formed-lambda-objectp but our hope is that mastering those details is
unnecessary because ACL2 provides a built-in ``macro,'' lambda$, for
constructing quoted well-formed LAMBDA objects. We urge you to use
lambda$ instead of typing quoted LAMBDA objects! That is, write
(lambda$ (x) (+ 1 x)) instead of '(LAMBDA (X) (BINARY-+ '1 X)).
Lambda$ terms may only appear in argument slots of ilk
:FN!
Examples:
(lambda$ (x y) (append x (list y)))
(lambda$ (n lst str)
(declare (type integer n)
(type string str)
(xargs :guard (and (posp n)
(true-listp lst)
(< (- n 1) (length lst)))))
(nth (- n 1) lst))
General Form:
(lambda$ vars dcl* body)
where the lambda$ expression occurs in an argument position of ilk
:FN, vars is a list of distinct variable names, dcl* is zero
or more DECLARE forms as described below, and body is a term
returning the appropriate number of values, which is currently always 1
except when used in the translation of an expression of the form (loop$
... DO ...). Body must satisfy the same restrictions one would expect
in a non-recursive defun event with the same formals, declarations
and body. In particular, body should contain no free variables other
than those listed in vars. Lambda$ always adds a declaration that
every formal is ignorable and, hence, we prohibit you from adding ignore
or ignorable declarations in the lambda$ expression itself.
Lambda$ expands to a well-formed quoted LAMBDA object or else
causes a translate-time error.
The allowed DECLARE forms in lambda$ are type and
xargs. Furthermore, the only xargs keywords allowed are
:guard and :split-types. The other XARGS keywords, such as
:measure, :hints or :guard-hints, play no role.
About Lambda$s and Prover Output
The translated form of a lambda$ expression is a quoted lambda object. For example, (collect$ (lambda$ (x) (+ 1 x)) lst)
translates to
(COLLECT$ '(LAMBDA (X)
(DECLARE (IGNORABLE X))
(RETURN-LAST 'PROGN
'(LAMBDA$ (X) (+ 1 X))
(BINARY-+ '1 X)))
LST)
The lambda$ has been replaced by a quoted lambda.
The prover tries to print each quoted lambda object (that occurs
an argument position of ilk :FN) as a lambda$
expression that is (provably) functionally equal (see fn-equal) to
the original lambda object assuming the necessary warrants. If the
quoted lambda object was produced by the expansion of a lambda$
expression and has not been simplified by subsequent rewriting, it will print
as the original lambda$ expression. This can be unfortunate if the
original lambda$ expression was itself produced by a macro and contains
logically irrelevant (but operationally important) tags. This phenomenon
occurs most often when do-loop$s are involved.
Furthermore, since you are allowed to type in quoted lambda objects
directly, you may — or may not — see them printed by the prover
as lambda$ expressions, depending on whether a suitable lambda$ is
found. If a quoted lambda object contains a reference to a function
symbol for which no warrant has been issued there is probably no
provably equivalent lambda$.
The main lessons here are
- you should use lambda$ rather than quoted lambda objects in
your prover input,
- you should make sure to warrant every user-defined function in your
lambda$ expressions, and
- if you see a quoted lambda object rather than a lambda$
expression in your prover output, that quoted lambda object probably
involves unwarranted symbols which will make it impossible to prove anything
interesting about it.
If you do not want the prover output to give special treatment to quoted
lambda objects in :FN slots, do
(defattach-system (untranslate-lambda-object-p
constant-nil-function-arity-0))
With this attachment, the prover will print all quoted lambda objects
as it would any other quoted constant. You will see what is actually there.
One drawback is that the resulting formulas cannot always be read back in
and translated because of a prohibition on ``counterfeiting'' expansions of
lambda$. See gratuitous-lambda-object-restrictions.
About Guard Verification of Lambda Objects
Quoted LAMBDA objects, whether produced by hand (don't!) or by
lambda$ may have guards. If the LAMBDA object is well-formed its
guard plays the same role the guard of a defined function symbol plays when
the object is apply$d. If the guard can be verified to imply the guards
of the body (which we call guard verification), and if the guard holds
of the actuals to which the object is applied (which we call guard
checking), a compiled version of the object is run. Otherwise, depending
on how set-guard-checking has been configured, either an error is
signaled or the object is interpreted under the axioms defining apply$
and ev$. Apply$ caches its investigations into guard
verification (but not guard checking) and compilation. We discuss the cache
in print-cl-cache.
When a guarded quoted LAMBDA object is used in a :FN slot of a
function definition, its guards are verified as part of the guard
verification step of defun or verify-guards. If that guard
verification fails, checkpoints will be printed and you can use
:guard-hints or :hints in the defun or verify-guards
events to supply the necessary guidance. When successful, the guard verified
LAMBDA objects in the defun are recorded in the cache.
But unlike defined function symbols, whose guards may be verified at
defun-time or at verify-guards-time, quoted LAMBDA expressions
may be introduced without an associated event. For example, the user may
simply type
ACL2 !>(apply$ (lambda$ (x)
(declare (type (satisfies natp) x))
(* x x))
'(5))
giving apply$ a LAMBDA object never before seen.
So apply$ must be ready to verify the guards of a quoted LAMBDA
object before attempting to apply it. This is in contrast to what happens
when apply$ is given a quoted function symbol. (Apply$ can just
look up whether a function symbol has been guard verified.)
To try to verify the guards of a quoted LAMBDA expression, apply$
limits itself to tau reasoning (see introduction-to-the-tau-system). The
idea is not to spend too much time making the decision as to whether compiled code
can be used or not. In addition, we don't want top-level evaluation, as shown
in the user type-in above, to provoke full-blown theorem proving.
Interpreting small quoted LAMBDA objects can be done relatively
quickly. After all, when the interpreter reaches a guard verified function
symbol inside the LAMBDA body it runs compiled code. It's only the body
itself that is interpreted.
But the tau system is pretty weak and so will be unable to verify some
non-trivial guard conjectures, which will mean the LAMBDA object is
interpreted. If the LAMBDA object is very large or is being being used
often, e.g., to map over a large object and check some property, you might
really want to invest the time to verify its guards. This can be done with
verify-guards, which as of Version 8.1 takes LAMBDA objects and
lambda$ terms and updates the cache. E.g.,
(verify-guards
(lambda$ (x)
(declare (type (satisfies natp) x))
(* x x)))
While this functionality is available to you, deciding that you need to
use it is problematic. Apply$ prints no warning that it has failed to
verify the guards of a LAMBDA object and is running interpreted code.
However, the utility print-cl-cache provides basic information about
the cache and its documentation may help you discover which LAMBDA
objects in use are unverified.
