		Search-engine friendly clone of the ACL2 documentation.

Loop$-primer

Lp-section-14

Challenge Problems about DO Loop$s

LP14: Challenge Problems about DO Loop$s

In this section you'll be asked to write and evaluate some DO loop$s based entirely on the examples given in the previous section. We'll deal with termination, guards, proofs, etc., later.

We want all iteration in your answers to be done with DO loop$s even if the problem could be solved with a FOR loop$.

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

——————————

LP14-1: Make a list of the integers from 10 down to 0.

Expected Value:(10 9 8 7 6 5 4 3 2 1 0)

Ok, we know this is a silly question if taken literally! Why use iteration at all if the answer is a constant? If you want to cheat, just enter

(loop$ with ans = '(10 9 8 7 6 5 4 3 2 1 0) do (return ans))

But the spirit of these questions is to use iteration and, if it helps, imagine we'd asked you to write a loop$ that returns the list of integers from 1000000 down to 0!

——————————

LP14-2: Sum the naturals less than or equal to 100.

Expected Value: 5050

Hint: Write the loop$ so that it counts down! If you count up you'll have to provide a measure term, which can be done by including :measure measure-term immediately after the DO operand and before the body.

——————————

LP14-3: Sum the squares of the naturals less than or equal to 100, using the following function to square.

(defun sq (x) (* x x))

Expected Value: 338350

——————————

LP14-4: Write a DO that finds the first occurrence of the symbol XXX in the list '(A B C XXX D E F) and returns the tail of the list starting with that occurrence.

Expected Value: (XXX D E F)

——————————

LP14-5: Fill in the blank below so that the next form is a theorem. You do not have to prove the theorem (but it shouldn't be hard).

(defun do-loop$-member (e lst)
  (loop$ ...))

(defthm lp14-5
  (equal (do-loop$-member e lst)
         (member e lst))
  :rule-classes nil)

——————————

LP14-6: Given the following

(defun steps-for-member (e lst steps)
  (cond ((endp lst) (list steps nil))
        ((equal (car lst) e) (list steps lst))
        (t (steps-for-member e (cdr lst) (+ 1 steps)))))

fill in the blank so that this is a theorem.

(defthm lp14-6
  (equal (loop$ ...)
         (steps-for-member e lst steps))
  :rule-classes nil)

——————————

LP14-7:Write a DO to compute the list of all pairs (i . j) such that 1 ≤ i ≤ 3 and 1 ≤ j ≤ 4.

Expected Value:

((1 . 1)
 (1 . 2)
 (1 . 3)
 (1 . 4)
 (2 . 1)
 (2 . 2)
 (2 . 3)
 (2 . 4)
 (3 . 1)
 (3 . 2)
 (3 . 3)
 (3 . 4))

——————————

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