Major Section: ACL2-BUILT-INS
Example LET Form:
(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.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 vali 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.
