Lp-section-9
Semantics of FOR Loop$s
LP9: Semantics of FOR Loop$s
For a thorough discussion of the semantics of FOR loop$s see
for-loop$, specifically the section “Semantics” which
includes two subsections, “Semantics of Simple Loop$s” and
“Semantics of Fancy Loop$s.” “Fancy” FOR
loop$s are FOR loop$s involving multiple iteration variables
and/or use of “global” (i.e., non-iteration) variables in the
loop$ body or the until or when clauses. We discuss DO
loop$s later. In this section of the primer we just present some
examples to drive home a few important points about FOR loop$s,
namely
- The semantics of a loop$ statement is obtained by translating the
loop$ statement, as with the command :trans.
- However, translation inserts a lot of tags into the formal term it
produced. These tags allow us to execute loop$ statements more
efficiently in the top-level ACL2 read-eval-print loop$. The tags on a
translated loop$, term, can be removed by the :tc (“translate and clean”) command and its variants :tca
and :tcp. When we exhibit semantics we typically show these simplified,
equivalent terms produced by one of these commands.
- The semantics of FOR loop$s look quite different from the
semantics of DO loop$s. Furthermore, the semantics of simple
loop$s have a different form than those of fancy loop$. So
“minor” changes in the syntax of a loop$ statement — the
addition of an AS clause, the use of global variable in the body of the
loop$, or the use of DO instead of, say, collect — can
cause radical changes in the form of the semantics.
- The semantics of loop$s always involve calls of scions on
lambda objects derived from the when, until, and loop$ body
clauses. The scions for simple FOR loop$s are sum$,
collect$, always$, thereis$, append$, until$, and
when$; the scions for fancy FOR loop$s are sum$+,
collect$+, always$+, thereis$+, append$+, until$+,
and when$+; and the scion for DO loop$s is do$.
- The iteration variables become formals of the lambda objects and
standard names are used in place of the user's names.
Now we drive home these points with some examples. The next section elaborates further.
Here is the full, formal translation of a simple FOR loop$.
ACL2 !>:trans (loop$ for x of-type integer in lst
when (evenp x)
collect (* x x))
(RETURN-LAST
'PROGN
'(LOOP$ FOR X OF-TYPE INTEGER IN LST
WHEN (EVENP X)
COLLECT (* X X))
(COLLECT$
'(LAMBDA (LOOP$-IVAR)
(DECLARE (TYPE INTEGER LOOP$-IVAR)
(XARGS :GUARD (INTEGERP LOOP$-IVAR)
:SPLIT-TYPES T)
(IGNORABLE LOOP$-IVAR))
(RETURN-LAST 'PROGN
'(LAMBDA$ (LOOP$-IVAR)
(DECLARE (TYPE INTEGER LOOP$-IVAR))
(LET ((X LOOP$-IVAR))
(DECLARE (IGNORABLE X))
(* X X)))
((LAMBDA (X) (BINARY-* X X))
LOOP$-IVAR)))
(WHEN$ '(LAMBDA (LOOP$-IVAR)
(DECLARE (TYPE INTEGER LOOP$-IVAR)
(XARGS :GUARD (INTEGERP LOOP$-IVAR)
:SPLIT-TYPES T)
(IGNORABLE LOOP$-IVAR))
(RETURN-LAST 'PROGN
'(LAMBDA$ (LOOP$-IVAR)
(DECLARE (TYPE INTEGER LOOP$-IVAR))
(LET ((X LOOP$-IVAR))
(DECLARE (IGNORABLE X))
(EVENP X)))
((LAMBDA (X) (EVENP X)) LOOP$-IVAR)))
LST)))
However, the logical meaning of this is easier to understand by
looking at one of the tc variations.
ACL2 !>:tc (loop$ for x of-type integer in lst
when (evenp x)
collect (* x x))
(COLLECT$ '(LAMBDA (LOOP$-IVAR)
(BINARY-* LOOP$-IVAR LOOP$-IVAR))
(WHEN$ '(LAMBDA (LOOP$-IVAR) (EVENP LOOP$-IVAR))
LST))
ACL2 !>:tcp (loop$ for x of-type integer in lst
when (evenp x)
collect (* x x))
(COLLECT$ (LAMBDA$ (LOOP$-IVAR)
(* LOOP$-IVAR LOOP$-IVAR))
(WHEN$ (LAMBDA$ (LOOP$-IVAR)
(EVENP LOOP$-IVAR))
LST))
ACL2 !>:tca (loop$ for x of-type integer in lst
when (evenp x)
collect (* x x))
(PROG2$
'(LOOP$ FOR X OF-TYPE INTEGER IN LST
WHEN (EVENP X)
COLLECT (* X X))
(COLLECT$ (LAMBDA$ (LOOP$-IVAR)
(DECLARE (TYPE INTEGER LOOP$-IVAR)
(XARGS :GUARD (INTEGERP LOOP$-IVAR)
:SPLIT-TYPES T))
(LET ((X LOOP$-IVAR))
(* X X)))
(WHEN$ (LAMBDA$ (LOOP$-IVAR)
(DECLARE (TYPE INTEGER LOOP$-IVAR)
(XARGS :GUARD (INTEGERP LOOP$-IVAR)
:SPLIT-TYPES T))
(LET ((X LOOP$-IVAR))
(EVENP X)))
LST)))
Note that :tc prints the term generated by translating the loop$
and then removing all tags. The guard and type declarations are logically
irrelevant. What you see is what the theorem prover will see
(if all the necessary warrants are assumed) before it starts to rewrite the
term. Note that the lambda object is just a quoted list constant and
the body has been translated so that the * macro was expanded in terms
of binary-*.
:Tcp (“p” for “pretty”) introduces familiar system macros.
:Tca (“a” for “annotations”) includes the original loop$
statement and shows declarations (if any) and the correspondence between the
user's iteration variable (x here) and the formal variable used in the
lambda objects generated (loop$-ivar here).
The translation of loop$ bodies into lambda objects standardizes
the variable name, either as loop$-ivar for simple loop$s which
have just one iteration variable, or as loop$-gvars and loop$-ivars
for fancy loop$s which may have one or more global variables and one or
more iteration variables. We'll deal with fancy loop$s immediately
below, but values are passed for loop$-gvars and loop$-ivars as tuples
listing all the global values and all the current iteration variable
values.
The advantage of this standardization is that choosing different names for
the iteration variables does not affect the formal semantics.
However, if we make a simple syntactic change, like introducing a global
variable by changing the body of the loop$ from (* x x) to (* x a),
where a is not an iteration variable, we drastically change the
semantics because we've converted the simple loop$ into a fancy
loop$. The (clean and pretty) semantics of
(loop$ for x in lst when (evenp x) collect (* x a))
is
(COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(* (CAR LOOP$-IVARS) (CAR LOOP$-GVARS)))
(LIST A)
(WHEN$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(EVENP (CAR LOOP$-IVARS)))
NIL
(LOOP$-AS (LIST LST))))
The annotated semantics of that loop$ is
(PROG2$
'(LOOP$ FOR X IN LST
WHEN (EVENP X)
COLLECT (* X A))
(COLLECT$+
(LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS)
(EQUAL (LEN LOOP$-GVARS) 1)
(TRUE-LISTP LOOP$-IVARS)
(EQUAL (LEN LOOP$-IVARS) 1))
:SPLIT-TYPES T))
(LET ((A (CAR LOOP$-GVARS))
(X (CAR LOOP$-IVARS)))
(* X A)))
(LIST A)
(WHEN$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS)
(EQUAL (LEN LOOP$-GVARS) 0)
(TRUE-LISTP LOOP$-IVARS)
(EQUAL (LEN LOOP$-IVARS) 1))
:SPLIT-TYPES T))
(LET ((X (CAR LOOP$-IVARS)))
(EVENP X)))
NIL
(LOOP$-AS (LIST LST)))))
Logically, we could have typed either of the above terms instead of the
fancy loop$. But operationally, the loop$ executes faster (when
guards are verified).
Notice that the simple scions COLLECT$ and WHEN$ have been
replaced by their fancy counterparts, COLLECT$+ and WHEN$+. The
lambda objects now have two formals, one for holding a tuple containing
all of the global variable values and one for a tuple holding all of the
current iteration variable values. The global variable value tuple, (LIST
A), is passed into the fancy scions if the corresponding lambda object
uses globals (as for the collect$+ but not for the when$+
lambda where NIL is passed instead). The list over which the
iteration variable ranges, LST, is now a list of tuples constructed by
LOOP$-AS. Finally, the bodies of the lambdas now access the
relevant values with CAR and CDR nests around the global and
iteration tuples. (No CDRs appear above because there is only one global
and one iteration variable in this example.)
The following similar but still fancier loop$ illustrates the general
situation. This loop$ has two iteration variables, x and y
taking on values from two ranges, xlst, and ylst, and uses two
global variables, a and b, in the body. We've added comments to
name the components of the two tuples.
ACL2 !>:tcp (loop$ for x in xlst
as y in ylst
when (evenp x)
collect (* x y a b))
(COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(* (CAR LOOP$-IVARS) ; x
(CADR LOOP$-IVARS) ; y
(CAR LOOP$-GVARS) ; a
(CADR LOOP$-GVARS))) ; b
(LIST A B)
(WHEN$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(EVENP (CAR LOOP$-IVARS))) ; x
NIL
(LOOP$-AS (LIST XLST YLST))))
Notice how the bodies of the lambda objects now use components of the
loop$-gvars and loop$-ivars) for the current values of the global
variables a and b and the iteration variables x and y.
The values of x and y are corresponding elements of xlst and
ylst as grouped together by (loop$-as (list xlst ylst)).
For a still-more elaborate FOR loop$ and a step-by-step
description of how the value of the formal semantics is computed, go to lp-section-10.
Now go to lp-section-10 (or return to the Table of Contents).
