Loop$-primer
Primer for using loop$
The Loop$ Primer
Preface
This primer was created at the request of and with the support of
Warren Hunt. It was originally conceived as a standalone document,
but it has been integrated into the ACL2 documentation to increase
its utility.
The ACL2 loop$ feature is an iteration primitive modeled on a
small subset of the Common Lisp loop facility. This documentation is
an elementary introduction to loop$ for use in both programming and proofs. We
assume the reader is already an experienced ACL2 user who is just new to
loop$.
Loop$ exploits ACL2's “higher order” capability using apply$. Logically, loop$ expressions are translated into calls of
scions or “mapping functions” that map one or more lambda objects over ranges. When loop$ expressions are typed into the
ACL2 top-level loop these formal semantics are executed, which can be
inefficient. When loop$ expressions are in guard verified (see verify-guards) functions they are compiled into Common Lisp loop
expressions and are executed very efficiently.
Two issues complicate the situation. First, Common Lisp's loop
facility is extraordinarily complex, requiring a full chapter of the reference
manual to explain. See loop
in the Common Lisp HyperSpec or Chapter 26 (pages 709-747) of Guy Steele's
monumental Common Lisp The Language, Second Edition. Second, ACL2's
logic is first-order, not higher-order, and so the apply$-based
semantics imposes restrictions that new users of ACL2 may find hard to deal
with.
This primer focuses on how to write loop$ expressions and how to prove things
about them. We start by asking you some questions that test your basic
knowledge of ACL2, so that you can decide whether this primer is right for
you. Then we discuss the so-called “FOR” loop$ and
later move on to the “DO” loop$. We follow the
“monkey see, monkey do” teaching style. We informally and
incompletely sketch the syntax and semantics, but we provide lots of examples
and we offer many challenge problems for you to solve. Answers are also
provided.
There are two glaring omissions in this primer: guard verification and the
use of stobjs in DO loop$.
While guard verification is crucial to the efficient execution of
loop$s by Common Lisp, we omitted much discussion of it because guard
obligations are generated automatically and are generally just
“ordinary” conjectures that we assume the experienced user can
figure out how to prove. The newcomer to loop$ may wonder “why am
I having to prove this?” but the answer is always the same: “the
Common Lisp compiler requires this in order for loop$ to behave like
loop.” Often the “fix” to a loop$ guard
verification problem is to add a :guard to the loop$ body,
remembering that it is translated into a lambda object that must be
guard verified in isolation since it might be passed around and applied in
many contexts. We include the syntax for loop$ guards.
We omitted much discussion of stobjs — which are allowed in DO
loop$s but not in other kinds of loop$s — because they raise
the same problems in DO loop$s as they do in “ordinary”
uses: syntactic single-threadedness into, through, and out of expressions.
We assume the experienced user knows how to deal with these issues.
There is a strong emphasis in this primer on problems for you to work on.
The best way to learn how to do something is to practice doing it!
The primer is divided into subjects listed in the Table of Contents which
is at the link lp-section-0. We recommend you read these sections in
the order shown. Each section ends with a pointer to the next section but
also includes a link to the Table of Contents.
Now go to lp-section-1. The Table of Contents is at lp-section-0.
Subtopics
- Lp-section-8
- Challenge Problems about FOR Loop$ in Defuns
- Lp-section-10
- The Evaluation of the Formal Semantics of a Fancy Loop$
- Lp-section-6
- Challenge Problems about FOR Loop$s
- Lp-section-9
- Semantics of FOR Loop$s
- Lp-section-17
- Challenge Proof Problems for DO Loop$s
- Lp-section-16
- Proving Theorems about DO Loop$s
- Lp-section-15
- Informal Syntax and Semantics of DO Loop$s
- Lp-section-11
- Proving Theorems about FOR Loop$s
- Lp-section-4
- Syntax of FOR Loop$s
- Lp-section-7
- Using Loop$s and Guards in Defuns
- Lp-section-13
- Examples of DO Loop$s
- Lp-section-12
- Challenge Proof Problems about FOR Loop$s
- Lp-section-14
- Challenge Problems about DO Loop$s
- Lp-section-5
- Informal Semantics of FOR Loop$s
- Lp-section-0
- Loop$ Primer Table of Contents)
- Lp-section-2
- Loop in Common Lisp and loop$ in ACL2
- Lp-section-18
- Conclusion
- Lp-section-3
- Examples of FOR Loop$s
- Lp-section-1
- Background Reviews
