Lp-section-2
Loop in Common Lisp and loop$ in ACL2
LP2: Loop in Common Lisp and loop$ in ACL2
The loop macro of Common Lisp was inspired by the “iterative
statements” in Warren Teitelman's CLISP package of Interlisp (1974). But
programming languages have had iterative statements since early in the
development of compilers. The first release of a FORTRAN compiler (1957)
supported what is probably the most well-known iterative construct, the “DO
loop.” But CLISP added many additional features including simultaneous
looping over multiple ranges, structured ways to filter the elements,
structured exit control mechanisms, and multiple ways to accumulate the
results. Common Lisp supports these and many other features.
ACL2's loop$ facility supports a tiny subset of Common Lisp's
loop statements. It is hard to overstate how small the ACL2 subset is!
For example, to manage iteration over a range of numbers, ACL2 provides
FROM, TO, and BY, but Common Lisp additionally provides
DOWNFROM,UPFROM,DOWNTO,UPTO,BELOW,and ABOVE.
For value accumulation, ACL2 supports SUM, COLLECT, APPEND,
ALWAYS, and THEREIS, while Common Lisp also supports NCONC,
COUNT, MAXIMIZE, and MINIMIZE. Even within its restricted
subset, ACL2 syntax is less flexible regarding the order of the various
“clauses” and the presence of, say, multiple accumulators. The list of
differences could go on and on because the Common Lisp facility is so
elaborate.
While many more Common Lisp loop features could be supported in ACL2,
we believe it is best to test and refine the techniques reasoning about
loop$ before elaborating it further.
Now go to lp-section-3 (or return to the
Table of Contents).
