Lp-section-7
Using Loop$s and Guards in Defuns
LP7: Using Loop$s and Guards in Defuns
Loop$ statements are most efficient when they are guard verified.
Loop$s typed at the top-level are typically not guard verified and so
they are not executed by running compiled Common Lisp loops. Instead,
their formal semantics is executed which is akin to saying they are
interpreted. But execution efficiency was one of the motivational factors in
the introduction of loop$ and that is best achieved by using loop$s
in guard verified function definitions.
Here is an example. We've already discussed member and the fact that
calls of member can be replaced by loop$s. Member is a macro
that expands logically to member-equal, where
(defun member-equal (x lst)
(declare (xargs :guard (true-listp lst)))
(cond ((endp lst) nil)
((equal x (car lst)) lst)
(t (member-equal x (cdr lst)))))
Let's define an equivalent function, named member-equal-loop$, using
loop$.
(defun member-equal-loop$ (x lst)
(declare (xargs :guard (true-listp lst)))
(loop$ for tail of-type (satisfies true-listp) on lst
thereis
(if (equal x (car tail)) tail nil)))
(defthm member-equal-loop$-is-member-equal
(equal (member-equal-loop$ x lst)
(member-equal x lst)))
Since member-equal has a guard of (true-listp lst), we will give
our member-equal-loop$ the same guard. But in our loop$ above we
also wrote that the iteration variable tail satisfies true-listp.
We do that so that ACL2 can prove the guard on (car tail) in the
thereis clause. (We could change ACL2 to infer this type for tail
in this special case, but more generally we would prefer to have an effective
heuristic for transferring arbitrary properties of lst to relevant
properties of tail.)
The guard obligations for member-equal-loop$ are obscure because we
haven't explained the formal semantics of loop$ yet. But we do not
discuss the guard obligations of loop$s in the primer. If you define a
function containing a loop$ and try to verify its guards the system will
generate the necessary obligations and try to prove them. Our solutions to
all the exercises in this primer can be guard verified automatically. For
more details on FOR loop$ guards and the guard obligations they generate,
see for-loop$, specifically, the sections “Special Guard Conjectures
for FOR Loop$s” and “Discussion of Why Loop$s Have Special
Guards.”
After admitting member-equal-loop$ ACL2 can prove inductively that it is
equal to member-equal. We'll come back to that later too.
An alternative way to specify the type of tail would be to add a :guard
rather than an of-type expression.
(defun member-equal-loop$ (x lst)
(declare (xargs :guard (true-listp lst)))
(loop$ for tail on lst
thereis
:guard (true-listp tail)
(if (equal x (car tail)) tail nil)))
The :guard feature of ACL2 is more flexible than of-type because
guards allow you to use multiple variables to express a constraint, while
of-type implicitly limits the assertion to the variable being
introduced. For example, with a guard you could say (subsetp-equal tail
lst) while you cannot express such a constraint with of-type.
However, of-type is understood by the Common Lisp compiler which might
optimize the compiled code using that type information, while guards are not
seen by the compiler.
When you use a loop$ in a defun to be guard verified, be sure to
constrain its iteration variables (and global variables) appropriately so you
can verify the guards of the body. (You are also allowed to specify
different guards for any when and until expressions.) We generally
split our constraints between of-type and :guard to inform the
compiler of simple types, while more elaborate guard conditions are sometimes
necessary to verify the guards of the body, etc. ACL2 will take any
of-type information and conjoin it to any :guard when doing guard
verification.
Now go to lp-section-8 (or return to the Table of Contents).
