Let
Binding of lexically scoped (local) variables
Introduction
Example
(let ((x (* x x))
(y (* 2 x)))
(list x y))
If the form above is executed in an environment in which x has the
value -2, then the result is '(4 -4).
Let expressions bind variables so that their ``local'' values, the
values they have when the ``body'' of the let is evaluated, are possibly
different than their ``global'' values, the values they have in the context in
which the let expression appears. In the let expression above, the
local variables bound by the let are x and y. They are locally
bound to the values delivered by the two forms (* x x) and (* 2 x),
respectively, that appear in the ``bindings'' of the let. The body of
the let is (list x y).
Suppose that the let expression above occurs in a context in which
x has the value -2. (The global value of y is irrelevant to
this example.) For example, one might imagine that the let form above
occurs as the body of some function, fn, with the formal parameter x
and we are evaluating (fn -2).
To evaluate the let above in a context in which x is -2, we
first evaluate the two forms specifying the local values of the variables.
Thus, (* x x) is evaluated and produces 4 (because x is
-2) and (* 2 x) is evaluated and produces -4 (because x is
-2). Then x and y are bound to these values and the body of
the let is evaluated. Thus, when the body, (list x y) is evaluated,
x is 4 and y is -4. Thus, the body produces '(4
-4).
Note that the binding of y, which is written after the binding of
x and which mentions x, nevertheless uses the global value of
x, not the new local value. That is, the local variables of the let
are bound ``in parallel'' rather than ``sequentially.'' In contrast, if
the example let* form:
(let* ((x (* x x))
(y (* 2 x)))
(list x y))
is evaluated when the global value of x is -2, then the result is
'(4 8), because the local value of y is computed after x has
been bound to 4. Let* binds its local variables
``sequentially.''
General let forms
(let ((var1 term1) ... (varn termn)) body)
and
(let ((var1 term1) ... (varn termn))
(declare ...) ... (declare ...)
body)
where the vari are distinct variables, the termi are terms
involving only variables bound in the environment containing the let, and
body is a term involving only the vari plus the variables bound in
the environment containing the let. Each vari must be used in
body or else declared ignored. In ACL2 the only declare
forms allowed for a let form are ignore, ignorable, and
type. See declare.
A let form is evaluated by first evaluating each of the termi,
obtaining for each a vali. Then, each vari is bound to the
corresponding vali and body is evaluated.
Actually, let forms are just abbreviations for certain uses of
lambda notation. In particular
(let ((var1 term1) ... (varn termn)) (declare ...) body)
is equivalent to
((lambda (var1 ... varn)
(declare ...)
body)
term1 ... termn).
Let* forms are used when it is desired to bind the vari
sequentially, i.e., when the local values of preceding varj are to be
used in the computation of the local value for vari.
General let* forms:
(let* ((var1 term1) ... (varn termn)) body)
and
(let* ((var1 term1) ... (varn termn))
(declare (ignore x1 ... xm))
body)
where the vari are variables (not necessarily distinct), the
termi are terms involving only variables bound in the environment
containing the let* and those varj such that j<i, and
body is a term involving only the vari plus the variables bound in
the environment containing the let*. Each vari must be used
either in some subsequent termj or in body, except that in the
second form above we make an exception when vari is among the xk, in
which case vari must not be thus used. Note that let* does not
permit the inclusion of any declare forms other than one as shown
above. In the second general form above, every xk must be among the
vari, and furthermore, xk may not equal vari and varj for
distinct i, j.
The first let* above is equivalent to
(let ((var1 term1))
...
(let ((varn termn)) body)...)
Thus, the termi are evaluated successively and after each evaluation
the corresponding vari is bound to the value of termi. The second
let* is similarly expanded, except that each for each vari that
is among the (x1 ... xm), the form (declare (ignore vari)) is
inserted immediately after ((vari termi)).
Each (vari termi) pair in a let or let* form is called a
``binding'' of vari and the vari are called the ``local variables''
of the let or let*. The common use of let and let*
is to save the values of certain expressions (the termi) so that they may
be referenced several times in the body without suggesting their
recomputation.
Let is part of Common Lisp. See any Common Lisp documentation for
more information.
