Lambda
Lambda expressions, LAMBDA objects, and lambda$ expressions
The word ``lambda'' occurs in several different contexts in ACL2.
When we are being precise our meanings are as outlined below.
- lambda expression -- This phrase is used to describe the syntactic
entity beginning with the symbol lambda that is allowed to occupy the
``function'' position in an ACL2 term. Lambda expressions are most
often created when let expressions are translated into their formal
counterparts. We provide an example below.
- LAMBDA object -- An ACL2 list constant interpreted as a ``function''
by apply$. LAMBDA objects may be written in terms by quoting them.
However, we urge the user to introduce LAMBDA objects into terms by using
the built-in macro lambda$. We provide examples below.
- lambda$ expressions -- These are untranslated terms beginning with
the macro symbol lambda$. They expand during translation to quoted LAMBDA
objects. We provide examples below.
These three phrases are very similar but mean very different things. You
should read carefully when you see us talk about lambda things!
Unfortunately, we're not always as precise as we might be so you might have
to disambiguate our usage by context. If you see places in the documentation
where you think we've messed up, please bring them to our attention!
About Lambda Expressions
Consider the function odd-evenp, defined with
(defun odd-evenp (x)
(if (zp x)
-1
(let ((ans (odd-evenp (- x 1))))
(* (+ ans 1) (- ans 1)))))
Distracting Aside: Can you see why we gave this function this name? Hint:
We might have named it ``weird evenp.''
The translated body of odd-evenp is
(if (zp x)
'-1
((lambda (ans)
(binary-* (binary-+ ans '1)
(binary-+ '-1 ans)))
(odd-evenp (binary-+ '-1 x))))
The syntactic entity in the function position of the term in the false
branch, namely
(lambda (ans)
(binary-* (binary-+ ans '1)
(binary-+ '-1 ans)))
is a lambda expression.
Lambda expressions are integral to the formal representation of terms.
They are the formal mechanism by which local variables are introduced and
thus allow repeated references to intermediate results without causing
recomputation. In ACL2 they obey the rules of Common Lisp. In particular,
while defining a recursive function it is allowed to call the function
recursively within the lambda expression, e.g., to temporarily save the value
of a recursive call for repeated use. (This is not illustrated by
odd-evenp where the recursive call is outside of the lambda expression.)
For more details on the formal representation of ACL2 terms, see term.
About LAMBDA Objects
Prior to Version 8.0 when apply$ was introduced, ``lambda
expression'' was the only phrase the ACL2 developers used mentioning the word
``lambda.'' Some Community Books introduced various terms or objects
mentioning the word but that is beyond the scope of this documentation.
Because ``lambda'' occurred in no other context before apply$ we are not
confident that every reference to what we are now calling ``lambda
expressions'' were called by that precise phrase in old documentation.
If you see a place where we refer to these entities by another phrase, please
let us know!
When apply$ was introduced, LAMBDA objects became a formally
supported concept in the ACL2 implementation and we started using
``LAMBDA objects'' to refer to them. A LAMBDA object is generally
a list, either of the form (LAMBDA vars body) or (LAMBDA vars dcl
body). There are additional restrictions on vars, dcl, and
body that we discuss later. But apply$ treats any consp
object and tries to extract those components by rudimentary pattern matching.
An example of a LAMBDA object is the list of length three
(LAMBDA (x) (BINARY-+ '1 X)).
Generally speaking when LAMBDA objects occur in translated terms they
are quoted, as in
(collect$ '(LAMBDA (X) (BINARY-+ '1 X)) lst)
To highlight the fact that these objects are constants, we try to write
them in UPPERCASE and typewriter font in this documentation. For the
same reason, we generally write ``LAMBDA object'' rather than ``lambda
object.''
But of course there's no difference between the symbol LAMBDA and the
symbol lambda. Furthermore, LAMBDA objects need not be quoted.
From a logical perspective they could just be consed up because they are just
ordinary ACL2 list constants. Their ``lambda'' status comes from being
treated as functions by apply$. So one could write
(collect$ (list 'lambda '(x) '(binary-+ '1 x)) lst)
and we would say that the value of the term in the first argument of
collect$ is a LAMBDA object.
Beware, however, that consing up LAMBDA objects defeats the ilk analysis in defwarrant and the tameness analysis of
apply$ and hence prevents functions containing such terms from being
apply$d.
According to the definitional axiom defining apply$, any object
satisfying consp is treated as a LAMBDA object. Apply$ uses
``accessor'' functions to extract the ``formals'' and ``body'' of the object
and proceeds to ev$ the body in an alist binding the formals. But
ev$ insists that the expression object being evaluated be tame or
else assigns it a default value. This insistence on tameness is due to
fundamental logical reasons; otherwise, apply$ would allow us to prove
NIL. So axiomatically apply$ operates as ``naively expected'' only
on tamep-lambdap objects. One consequence of this, which we expect will
be a minor inconvenience, is that unlike ACL2's lambda expressions
apply$'s LAMBDA objects, when used in definitions of new functions,
may not include recursive calls of the function being defined because they
fail the tameness test.
But wait! There's more. Execution efficiency of apply$ imposes some
non-logical restrictions. These restrictions come from ACL2's execution
story with respect to Common Lisp, and from the Common Lisp compiler. To
execute LAMBDA objects most efficiently they must be well-formed, which
is a concept even stronger than tameness. Among other requirements,
well-formed LAMBDA objects obey the ACL2 and Common Lisp rules on
variable names (not every symbol is a legal variable), on the use of free
variables, on the body being a fully translated formal term, that the
declarations, if any, be meaningful to the Common Lisp compiler, etc. You
can read about well-formedness in well-formed-lambda-objectp if you
want, but we don't encourage beginners to go there!
Note: Even well-formedness is not enough to guarantee execution of
compiled code. The LAMBDA object must also be guard verified (see
verify-guards for a discussion) and its guard must be satisfied by
the arguments to which it is applied.
Note: A peculiar aspect of LAMBDA objects is that they can be written
as legal ACL2 constants before they are well-formed LAMBDA
objects, e.g., by referring to undefined functions, :program mode
functions, unbadged functions, etc. They are, after all, just arbitrary
quoted objects and any value in ACL2 can be quoted. An ill-formed
LAMBDA object can become well-formed if the world is
appropriately extended, e.g., the appropriate defuns or
defwarrants are made. Perhaps worse, they can be well-formed and then
become ill-formed by an undo. So at runtime apply$ has to check
that the function symbol or LAMBDA object is appropriate. There is a
sophisticated cache behind the execution machinery for LAMBDA objects in
the evaluation theory. See print-cl-cache.
About Lambda$ Expressions
Rather than force users to type well-formed LAMBDA objects as quoted
constants, ACL2 provides a macro allowing you to enter LAMBDA objects by
typing something that looks like a lambda expression but which is properly
translated and generates well-formed results (or causes a translation
error).
That macro -- which is not really a defined macro but is built into ACL2's
translation mechanism -- is called lambda$ and uses of it in terms
are called ``lambda$ expressions.'' Lambda$ expressions may only be
used in argument slots of ilk :FN.
An example of a lambda$ expression is the first argument of
collect$ in
(collect$ (lambda$ (x) (+ 1 x)) lst)
That lambda$ expression essentially translates to the quoted
well-formed LAMBDA object
'(LAMBDA (X) (BINARY-+ '1 X))
Note that the body is fully translated, unlike its appearance in the
lambda$ expression. We say ``essentially'' because lambda$ always
add a (DECLARE (IGNORABLE v1 ... vn)) that includes every formal. In
addition, except when translating in theorems, lambda$ tags the
translated body with a return-last expression to indicate it came
from a lambda$. Despite these differences, the meaning of the
translated lambda$ is the simple quoted LAMBDA object shown.
Lambda$ expressions never appear in a fully translated term. All the
lambda$ objects will have been translated into quoted LAMBDA
objects.
The body of a lambda$ expression must return a single value that is
neither a stobj nor a df. The following example illustrates
this point.
(defun$ f1 (x)
(declare (xargs :guard t))
(mv x x))
; ERROR! The body of the lambda$ returns two values.
(defun f2 (y)
(declare (xargs :guard t))
(apply$ (lambda$ (x) (f1 x))
(list y)))
; Succeeds.
(defun f2 (y) (declare (xargs :guard t))
(apply$ '(lambda (x) (f1 x))
(list y)))
Finally, to see how a lambda$ expression translates, see translam.
