Lp-section-10
The Evaluation of the Formal Semantics of a Fancy Loop$
LP10: The Evaluation of the Formal Semantics of a Fancy Loop$
Below we show the evaluation of a fancy loop$ that uses the function
packn to create a list of symbols. We start with an example of
packn so you can infer its behavior. But our real interest is the
behavior of the loop$.
ACL2 !>(packn (list 'R2 '- 'D 2))
R2-D2
ACL2 !>(let ((mark '*))
(loop$ for x in '(a * b c d e * f g h i j * k)
as y in '(u v * w * u v * x y z)
as i from 0 to 100 by 3
when (and (evenp i)
(not (eq x mark))
(not (eq y mark)))
collect (packn (list x y '_ i))))
(AU_0 GX_24 IZ_30)
ACL2 !>
We now explain carefully the evaluation of the loop$ expression above
in an environment in which mark is bound to the asterisk symbol,
*.
The first three lines of the loop$ introduce the so-called iteration
variables, x, y, and i, and their respective
ranges.
The when clause specifies a predicate on the iteration variables,
identifying the “good” cases, i.e., the values of the iteration variables
that we care about. However, note that the predicate above mentions the
variable mark, which is not one of the iteration variables. We call
such variables globals because their values are not set within the
scope of the loop.
The collect clause specifies an expression to be evaluated on the
“good” iteration variable values and collects the results of those
evaluations.
If you replace the symbol loop$ above by loop you get a legal
Common Lisp loop expression with the same value (if executed when
mark is bound to *).
For our purposes, the easiest way to think about this particular statement
is to decompose it into three steps.
Step 1: The lines introducing the iteration variables and their ranges
cause us to make a table of corresponding values of x, y, and
i, as shown below in the form of a list of triples. This list is as
long as the shortest individual range.
; x y i
((A U 0)
(* V 3)
(B * 6)
(C W 9)
(D * 12)
(E U 15)
(* V 18)
(F * 21)
(G X 24)
(H Y 27)
(I Z 30)).
Step 2: the when clause maps over the above table and identifies the
entries as “good” or “bad”, where the good ones have an even value for
i and values for x and y that are not the asterisk mark,
*. We annotate the table accordingly below.
; x y i
((A U 0) ; GOOD!
(* V 3) ; bad: odd i (and asterisk)
(B * 6) ; bad: asterisk
(C W 9) ; bad: odd i
(D * 12) ; bad: asterisk
(E U 15) ; bad: odd i
(* V 18) ; bad: asterisk
(F * 21) ; bad: odd i (and asterisk)
(G X 24) ; GOOD!
(H Y 27) ; bad: odd i
(I Z 30)). ; GOOD!
Effectively the when clause pares down the table to just the good
entries.
; x y i
((A U 0) ; GOOD!
(G X 24) ; GOOD!
(I Z 30)). ; GOOD!
Step 3: the collect clause maps over pared-down table, evaluating and
collecting the results of (packn (list x y '_ i)) for each triple in the
table.
(AU_0
GX_24
IZ_30).
The ACL2 semantics of the loop$ statement reflects this understanding
of the statement. (The display below is the output of :tca on the
loop$, but with the DECLARE forms deleted and the three comments
added.)
(collect$+ ; step 3
(lambda$ (loop$-gvars loop$-ivars)
(let ((x (car loop$-ivars))
(y (cadr loop$-ivars))
(i (caddr loop$-ivars)))
(packn (list x y '_ i))))
nil
(when$+ ; step 2
(lambda$ (loop$-gvars loop$-ivars)
(let ((mark (car loop$-gvars))
(x (car loop$-ivars))
(y (cadr loop$-ivars))
(i (caddr loop$-ivars)))
(and (evenp i)
(not (eq x mark))
(not (eq y mark)))))
(list mark)
(loop$-as (list '(a * b c d e * f g h i j * k) ; step 1
'(u v * w * u v * x y z)
(from-to-by 0 100 3)))))
In step 1, the loop$-as function takes a list of the individual
ranges and builds the first version of the iteration variable table. The
function from-to-by just enumerates the integers from its first argument
to its second argument in steps of size given by its third argument.
In step 2, the when$+ function takes three arguments. Note that the
last argument of the when$+ function is the iteration variable table
computed by step 1. The first argument of the when$+ function is a
lambda$ expression representing the predicate used to identify the
“good” entries. But that predicate may also require the value of any
global variables used. So the lambda$ expression has two arguments,
loop$-gvars, the list of values of the global variables, and
loop$-ivars, a tuple of values corresponding to a line in the iteration
variable table. The middle argument of the when$+ provides the values
of the global variables and, as noted earlier, the last argument is the
iteration variable table. The when$+ maps over the iteration variable
table and collects the “good” lines, returning them as a list.
In step 3, the collect$+ takes three arguments. The first is a
lambda$ expression on the loop$-gvars and loop$-ivars as
above. The second and third arguments are the global variable values and the
“good” lines from the pared-down iteration variable table as computed by
step 2. Note that since the collect clause does not mention any global
variables the global variable tuple in the second argument of the
collect$+ is nil.
Of course, Common Lisp does not decompose the corresponding loop
statement this way but generates much more efficient compiled code.
The ACL2 semantics is rendered compositionally to make it easier to reason
about loop$ statements. If the guards of the loop$ statement
— which we haven't discussed yet — are verified then the ACL2
loop$ statement is rendered into the corresponding Common Lisp loop
statement, compiled, and efficiently executed.
Now go to lp-section-11 (or return to the Table of Contents).
