		Search-engine friendly clone of the ACL2 documentation.

Loop$-primer

Lp-section-8

Challenge Problems about FOR Loop$ in Defuns

LP8: Challenge Problems about FOR Loop$ in Defuns

Do the problems below, starting in a fresh ACL2 session that starts with the standard (include-book "projects/apply/top" :dir :system). Each problem starts with one or more recursive functions. Admit those functions in your session. Then define equivalent versions using loop$s instead of recursion. Make sure each of your defuns is admitted and guard verified. Try to ensure that the loop$ version is unconditionally equal to the recursive version of each function. But you might find more elegant solutions if you're willing to condition your equivalences on the guards of the recursive versions. After all, a main motivation for using loop$ is the runtime efficiency of the compiled raw Lisp, and since no ACL2 function is executed in raw Lisp unless the guards are verified.

Finally, you need not use ACL2 to prove that your loop$ functions correctly implement their recursive counterparts. But you should be aware that with a few exceptions the proofs of our solutions were completely automatic. We'll focus on proving theorems about loop$s later in the primer.

Our answers to the problems in this section are in community-books file demos/loop-primer/lp8.lisp.

——————————

Sample Question: (Sum-vals alist) sums the value components of an alist. Note its guard.

(defun symbol-to-integer-alistp (x)
  (declare (xargs :guard t))
  (if (atom x)
      (equal x nil)
      (and (consp (car x))
           (symbolp (caar x))
           (integerp (cdar x))
           (symbol-to-integer-alistp (cdr x)))))

(defun sum-vals (alist)
  (declare (xargs :guard (symbol-to-integer-alistp alist)))
  (cond ((endp alist) 0)
        (t (+ (cdar alist) (sum-vals (cdr alist))))))

E.g., (sum-vals '((a . 1) (b . 2) (c . 3))) = 6.

Define sum-vals-loop$ so that it is unconditionally equivalent to sum-vals but uses loop$ instead of recursion.

Sample Solution:

(defun sum-vals-loop$ (alist)
  (declare (xargs :guard (symbol-to-integer-alistp alist)))
  (loop$ for pair in alist
         sum
         :guard (and (consp pair)
                     (integerp (cdr pair)))
         (cdr pair)))

The (consp pair) in the loop$ :guard is necessary because the loop$ body contains (cdr pair) and Common Lisp expects cdr to be applied to a consp or nil. The (integerp (cdr pair)) is necessary because the value of the loop$ body is being summed and so must be (at least) a number to satisfy Common Lisp's expectation on +.

Verification of Sample Solution:

(defthm sum-vals-loop$-is-sum-vals
  (equal (sum-vals-loop$ alist)
         (sum-vals alist))
  :rule-classes nil)

It is conceivable in some Common Lisps that the following would compile into more efficient code.

(defun sum-vals-loop$ (alist)
  (declare (xargs :guard (symbol-to-integer-alistp alist)))
  (loop$ for pair of-type cons in alist
         sum
         :guard (integerp (cdr pair))
         (the integer (cdr pair))))

The thinking is that the of-type cons and (the integer (cdr pair)) could in principle allow the compiler to do type checking that could eliminate runtime tests to avoid errors. That's because of-type and the are Common Lisp primitives, as are the particular type-specs used in sum-vals-loop$. Whether such a well-declared version of sum-vals-loop$ would actually run faster on your Common Lisp depends on the compiler and the optimization proclamations. In CCL and SBCL with ACL2's default proclamations, this well-declared version runs no faster than the original sample solution does. We raise this point simply to alert the reader to the difference between compiler directives and :guards.

——————————

LP8-1 Define sum-vals-loop$ which is like our solution shown for sum-vals above, except instead of using symbol-to-integer-alist as the :guard write the :guard as (and (true-listp alist) (loop$ ...)). Be sure your definition is admitted and guard verified.

If you want a slightly more challenging problem, omit the (true-listp alist) from the :guard and use a FOR loop$ “ON” alist. FYI: Common Lisp requires “IN” loop$s to be over a true-listp target, but there is no such requirement for “ON” loop$s.

You can always convert an “IN” loop$ governed by a true-listp check to an “ON” loop$ without the check. See our solutions. But because of that, we'll use the more elegant “IN” solutions in the rest of these problems.

——————————

LP8-2 The recursive function below is in the ACL2 sources (therefore, you will not have to define it in your session). Define an equivalent function, named arglistp1-loop$ that uses loop$ instead of recursion.

(defun arglistp1 (lst)
  (declare (xargs :guard t))
  (cond ((atom lst) (null lst))
        (t (and (legal-variablep (car lst))
                (arglistp1 (cdr lst))))))

Why is arglistp1-loop$ a little less efficient than arglistp?

——————————

LP8-3 The two recursive functions below are used in the ACL2 sources (thus, you won't have to define them in your session). Define packn1-loop$ that is equivalent to packn1 but so that it uses loop$s and does not mention atom-listp.

(defun atom-listp (lst)
  (declare (xargs :guard t
                  :mode :logic))
  (cond ((atom lst) (eq lst nil))
        (t (and (atom (car lst))
                (atom-listp (cdr lst))))))

(defun packn1 (lst)
  (declare (xargs :guard (atom-listp lst)))
  (cond ((endp lst) nil)
        (t (append (explode-atom (car lst) 10)
                   (packn1 (cdr lst))))))

——————————

LP8-4 Define select-corresponding-element-loop$ so that it is equivalent to select-corresponding-element, below, but using a loop$ statement.

(defun select-corresponding-element (e lst1 lst2)
  (declare (xargs :guard (and (true-listp lst1)
                              (true-listp lst2)
                              (not (member nil lst2)))))
  (cond
   ((endp lst1) nil)
   ((endp lst2) nil)
   ((equal e (car lst1)) (car lst2))
   (t (select-corresponding-element e (cdr lst1) (cdr lst2)))))

For example,

(select-corresponding-element
  'wednesday
  '(sunday monday tueday wednesday thursday friday saturday)
  '(dimanche lundi mardi mercredi jeudi vendredi samedi))
=
'MERCREDI

——————————

LP8-5 Define same-mod-wildcard-loop$ to be equivalent to same-mod-wildcard, below, but using a loop$ statement.

(defun same-mod-wildcard (lst1 lst2)
  (declare (xargs :guard (and (true-listp lst1)
                              (true-listp lst2)
                              (equal (len lst1) (len lst2)))))
  (cond ((endp lst1) t)
        ((or (eq (car lst1) '*)
             (eq (car lst2) '*))
         (same-mod-wildcard (cdr lst1) (cdr lst2)))
        ((equal (car lst1) (car lst2))
         (same-mod-wildcard (cdr lst1) (cdr lst2)))
        (t nil)))

For example,

(same-mod-wildcard '(a * c d *) '(a x c * d))
=
T

——————————

LP8-6 The following function is part of the ACL2 source code, so you don't have to define it in your session.

(defun getprops1 (alist)
  (declare (xargs :guard (true-list-listp alist)))
  (cond ((endp alist) nil)
        ((or (null (cdar alist))
             (eq (car (cdar alist))
                 *acl2-property-unbound*))
         (getprops1 (cdr alist)))
        (t (cons (cons (caar alist) (cadar alist))
                 (getprops1 (cdr alist))))))

Define getprops1-loop$ to do the same thing using loop$.

——————————

Now go to lp-section-9 (or return to the Table of Contents).