Lp-section-15
Informal Syntax and Semantics of DO Loop$s
LP15: Informal Syntax and Semantics of DO Loop$s
The “most elaborate” DO loop$ looks like this.
(LOOP$ WITH var1 OF-TYPE spec1 = init1 ; a WITH declaration
WITH var2 OF-TYPE spec2 = init2
...
DO
:measure m
:guard do-guard
:values v
do-body
FINALLY
:guard fin-guard
fin-body)
where much of that is optional: “OF-TYPE speci”,
“= initi” (when “OF-TYPE speci” is
present), “:MEASURE m”, the two “:GUARD
...” clauses, “:VALUES v”, and “FINALLY
fin-body”. If the :MEASURE is omitted, ACL2 tries to guess a
likely measure using the same heuristic it does with recursive defuns. If :VALUES is omitted then v defaults to (nil).
All ACL2 function symbols in m, do-body, and fin-body must
be badged so apply$ can handle them. Furthermore, they must
be warranted if proofs are to be done about them or if they are in
logic mode and are called during evaluation.
As you've already inferred from our examples, do-body and
fin-body are not normal ACL2 terms! They allow restricted uses of
RETURN, PROGN, SETQ, MV-SETQ, and LOOP-FINISH.
As for semantics, every legal DO loop$ translates into a term
of the form
(DO$ m-lambda
alist
do-body-lambda
fin-body-lambda
a5
a6)
where m-lambda, do-body-lambda, and fin-body-lambda are
quoted LAMBDA objects derived from the respective terms in the
loop$ statement. Alist is an association list that maps the
variables of those terms to their initial values. We discuss the other three
arguments later.
All three of these LAMBDA objects operate on alist. The
m-lambda may return a natural, and otherwise must return a list of naturals which is treated as a
lexicographic tuple whose first component is the most significant. The other
two LAMBDA objects return a triple of the form (exit-token value
new-alist). The exit-token is :RETURN, :LOOP-FINISH, or
NIL, and indicates what happens next: the value is to be returned
as the value of the loop$, the fin-body-lambda is to be applied to
the new-alist, or the loop$ is to iterate again on new-alist.
But before the iteration, the m-lambda is applied to the new-alist
and must be of smaller measure according to l< for iteration to
continue.
If the given measure fails to decrease, then, logically speaking, a5
is used to compute a default answer. (That argument is actually the output
signature of the loop$ specifying how many values are to be returned and
whether each value is an ordinary object, a double-float, or a stobj.)
However, in execution, an error is signaled if the measure fails to decrease.
Such runtime errors (including OF-TYPE and guard violations if guards
are being checked) are reported using a6 which is just a
quoted constant about the original loop$ statement. (In fact, a6
is logically irrelevant and the theorem prover replaces quoted non-nil
final argument to do$ by nil in proofs as part of the cleaning-up
process.)
Consider this simple DO loop$ and its cleaned-up semantics as
shown by the :tcp command. (We have re-pretty-printed it
to add comments and highlight some symmetries.)
ACL2 !>:tcp (loop$ with i = n
with ans = 0
do
(if (zp i)
(return ans)
(progn (setq ans (+ 1 ans))
(setq i (- i 1)))))
(DO$
; measure lambda:
(LAMBDA$ (ALIST)
(ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'I ALIST))))
; initial alist:
(LIST (CONS 'I N)
(CONS 'ANS 0))
; do-body lambda:
(LAMBDA$ (ALIST)
(IF (ZP (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(LIST :RETURN
(CDR (ASSOC-EQ-SAFE 'ANS ALIST))
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST)))))
(LIST NIL
NIL
(LIST (CONS 'I (+ -1 (CDR (ASSOC-EQ-SAFE 'I ALIST))))
(CONS 'ANS (+ 1 (CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))))
; fin-body lambda (irrelevant here)
(LAMBDA$ (ALIST)
(LIST NIL
NIL
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))
; irrelevant args a5 and a6
'(NIL) NIL)
ASSOC-EQ-SAFE is just ASSOC-EQ with a slightly weaker guard.
Think of (CDR (ASSOC-EQ-SAFE 'var ALIST)) as the current value of the
local variable var. The measure is that the ACL2-COUNT of the
current value of I decreases. The output of the do-body
lambda is a triple. The true branch of the IF indicate iteration
is to stop and return the current value of ANS. The false branch
indicates iteration is to continue with the new alist given as the third
element of the triple. The fin-body lambda is irrelevant because
there is no :LOOP-FINISH exit in the do-body.
Of course, the semantics of do$ is explicit in its definition.
So you might want to execute :pe do$ in your ACL2 session and just
read how do$ operates.
We realize the above descriptions are pretty sketchy. But in the coming
discussions and proof problems we'll limit ourselves to DO loop$s
without of-types or guards, they'll all return single non-stobj values so the :values option won't be needed, and you won't really
need to use the finally clause or any fancier bodies than we show in our
examples.
For more details about both the syntax and semantics of DO
loop$s see do-loop$. But beware! That link takes you out of
the loop$ primer! To get back here either use your browser's
“back” button or remember to return to lp-section-15!
Now go to lp-section-16 (or return to the Table of Contents).
