LET

binding of lexically scoped (local) variables
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.