Lp-section-6
Challenge Problems about FOR Loop$s
LP6: Challenge Problems about FOR Loop$s
The questions below ask you to write and evaluate some FOR
loop$s at the top-level of ACL2.
Our answers to the problems in this section are in community-books
file demos/loop-primer/lp6.lisp. Feel free to look at our answers after
you have worked on a problem. But remember: reading an answer is not as
helpful as finding it yourself. If you give up on a problem, look at our
answer for just that problem, so maybe you take a little more insight into
your work on subsequent problems.
Don't forget to start your session by including the standard book for
apply$.
(include-book "projects/apply/top" :dir :system)
Don't bother with adding :guard expressions and don't define any
functions of your own yet. All of these questions can be answered by
loop$ expressions involving only ACL2 primitives and the constant
function bags which we introduce below for convenience.
Let a “bag” be a true list of symbols. The function below returns a
constant list of bags. You may use (bags) in your solutions. Notice
that some elements of (bags) contain the symbol x and other do
not.
(defun bags ()
'((a b c)
(d x e f)
(g h i x)
(j)
(x k l)))
Here is a sample question and how you might check that your loop$
computes the expected value.
——————————
Sample Question: Build an alist that pairs the first symbol in every bag
of (bags) with the number of other symbols in the bag. The expected
value is ((A . 2) (D . 3) (G . 3) (J . 0) (X . 2)).
Sample Check of a Solution:
(equal (loop$ for bag in (bags)
collect (cons (car bag) (len (cdr bag))))
'((A . 2) (D . 3) (G . 3) (J . 0) (X . 2)))
Of course, you could just type the loop$ statement at the top-level
of your ACL2 session and visually inspect the answer. If you want to
make a certified book out of your answers we recommend expressing the
checks as defthm events of :rule-classes nil, as in
(defthm check-sample-question
(equal (loop$ for bag in (bags)
collect (cons (car bag) (len (cdr bag))))
'((A . 2) (D . 3) (G . 3) (J . 0) (X . 2)))
:rule-classes nil)
However, if your loop$ involves a user-defined function and you
express your answers as defthms then each theorem will need to have
appropriate warrant hypotheses, as illustrated below.
(defun my-len (x) (if (atom x) 0 (+ 1 (my-len (cdr x)))))
(defwarrant my-len)
(defthm check-my-sample-question
(implies (warrant my-len)
(equal (loop$ for bag in (bags)
collect (cons (car bag) (my-len (cdr bag))))
'((A . 2) (D . 3) (G . 3) (J . 0) (X . 2))))
:rule-classes nil)
——————————
LP6-1: Concatenate all the bags in (bags).
Expected Value:(A B C D X E F G H I X J X K L)
——————————
LP6-2: Collect the bags that contain the symbol x.
Expected Value:((D X E F) (G H I X) (X K L))
——————————
LP6-3: If you used some version of member in your solution to
LP6-2, now do it without using any version of member.
Expected Value:((D X E F) (G H I X) (X K L))
Don't use any version of member in your answers to the remaining
questions in this section.
——————————
LP6-4: Remove all the xs from each bag in (bags) and
concatenate the resulting bags.
Expected Value:(A B C D E F G H I J K L)
——————————
LP6-5: Collect the first symbol of each of the bags in (bags)
that contains an x.
Expected Value:(D G X)
——————————
LP6-6: From each bag in (bags), remove the elements
preceding the first x and collect the resulting bags.
Expected Value:(NIL (X E F) (X) NIL (X K L))
——————————
LP6-7: Let's say the “alternating sum of signed squares” of a
list of numbers is the sum of the squares of the elements, except the squares
of elements in even positions (0-based) are added and the squares in odd
positions are subtracted. So the alternating sum of signed squares of (1
2 3 4 5) is (+ 1 -4 9 -16 25) = 15. Compute the alternating sum
of signed squares of the lengths of the bags in (bags)
Expected Value:(+ 9 -16 16 -1 9) = 17.
——————————
LP6-8: Collect all the function symbols in the current ACL2
world with an arity greater than 9.
Three Hints: First, the term (function-theory :here) returns a list
of the runes of all the :logic mode functions currently in the ACL2
world. However, it expands to an expression involving the variable
world which can be obtained by (w state). And state may
not be used in FOR loop$! So you'll have to let bind
world to (w state) and write your loop$ inside the scope of
that let.
Second, every rune returned by function-theory is of the form
(:DEFINITION fn . x), where fn is the name of a function.
Third, the arity of a symbol fn is obtained from the world by
(arity fn world), except sometimes (for reasons we won't go into!) it
returns nil.
Expected Value: As of ACL2 Version 8.5 (after including the
"projects/apply/top" book) the answer was (MEMOIZE-FORM SEARCH-FN
SEARCH-FN-GUARD BUILD-STATE1), but that may change.
——————————
LP6-9: Collect the name of every theorem about EXPT in the
current world.
Three More Hints: First, the ACL2 world is a list of triples of the form
(name property . val) representing the current property lists. In ACL2
Version 8.5, the length of the world (after including the
"projects/apply/top" book) is 137,846, so it's too big to just look
at!
Second, each event that named a theorem has a triple of the form (name
THEOREM . val), where name is the event name and val is the
translated version of the theorem. (Thus, you won't find macros like +
or append in val! Instead it would contain the function symbols
appearing in their expansions, e.g., binary-+ and binary-append.
But since we're looking for expt and it is not a macro, this doesn't
matter.)
Third, the ACL2 term (all-fnnames term) returns a list of all the
function symbols used in the fully translated term term.
Expected Value: As of ACL2 Version 8.5 (after including the
"projects/apply/top" book) the answer was
(APPLY$-PRIM-META-FN-EV-CONSTRAINT-462 RATIONALP-EXPT-TYPE-PRESCRIPTION
EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE)
——————————
These exercises highlight three important lessons about
loop$.
The first is that with loop$ you can avoid defining a lot of
recursive functions. Imagine doing these same exercises without
loop$.
The second is that it is not always a good idea to “inline” loop$s
instead of defining functions. The clearest example of that arises above
when we prohibited you from using member! Just because member can
be replaced by a loop$ doesn't mean it should be! Member is an
exceptionally useful function that enjoys a lot of elegant properties. By
introducing the name member and proving its properties we can use it
conveniently and appeal to those properties often. Of course, member is
a Common Lisp primitive, so we're not free to define it, but if we were to
define a function like that we could use a loop$ in its definition.
Another example of this second lesson is in question LP6-7. Depending on
the project at hand, the notion of “alternating sum of signed squares”
might be a useful one in its own right. So perhaps if such a problem came up
you might define (alternating-sum-of-signed-squares lst), perhaps using
loop$ in the defun, and then use
(alternating-sum-of-signed-squares
(loop$ for bag in (bags) collect (len bag)))
to compute the quantity requested in LP6-7.
The question raised by this second lesson isn't so much whether you use a
loop$ to express the concept but whether you use a defun to give
the concept a name. A good rule of thumb is: if the concept has a natural
name, define it!
Of course, there is the usual trade-off between execution efficiency and
modularity. There are various ways to deal with this trade-off in ACL2 but
since they are not unique to loop$ we won't discuss them.
The third lesson is highlighted by LP6-8 and LP6-9. Loop$ can be
very useful in extracting data about your current ACL2 session, if you are
familiar with the ACL2 system-level utilities (see system-utilities
for some of them). Perhaps more relevant is the observation that if you are
building a big model involving lots of data, you might find loop$ handy
in querying your own data.
Now go to lp-section-7 (or return to the Table of Contents).
