List Question

Hi there,

I just recently started learning ACL2 and I have run into a problem.
I am trying to test if something is a list-of-lists-of-lists.
Example:

(((1 2 3) (1 2 3)) ((4 5 6) (4 5 6)))

(The lists of 1 2 3 are grouped in a list, and the lists of 4 5 6 are group in a list, all contained within a list).
I know of true-listp, and true-list-listp. Is there a way I can test this without recursion?

If you really mean "list-of-lists-of-lists", then you can do it by straightforwardly applying car and cdr.

If you mean to an arbitrary depth, here is the problem you're solving. If you could do a test of constant depth (say, consp) and then move on to only one place (say, the cdr), then conversion to an iteration is obvious.

But in this case you need to suspend the future execution (moving on to the cdr and continuing the test) and perform the arbitrary-depth test (on the car, testing whether it is a list of...). This is what execution stacks do: they preserve your local data, and you have to push the instruction pointer before descending into a new function call, so the system can resume your future execution once the call completes.

Understanding this, you can convert this, and all other recursion problems, to explicitly model future execution suspension. Since you have two paths at every test point, and can only follow one of them at a time, you need to find a way to enqueue the other so you can test it once you finish the first path. Thinking about the previous paragraph should help you model this.

Well, first question: is this homework? In any case, that is an interesting problem.

There is a function named EVERY. It takes a function and a list and applies that function to every element of that list. If every call to the function returns true, it returns T, otherwise it returns NIL. For instance, this tests if LIST is a list of odd numbers:

(every #'oddp list)

If I understood correctly, you can test if something is a list (and not a list of lists) with TRUE-LISTP. In any case it would be something like this:

(defun true-listp (list)
  (and (listp list)
       (every #'atom list)))

So, I guess that TRUE-LIST-LISTP is supposed to test if something is a list of lists? Well, that is not hard to do as well:

(defun true-list-listp (list-of-lists)
  (and (listp list-of-list)
       (every #'true-listp list-of-lists)))

It should be easy to extract the solution from the pattern you see here. You might or might not want to iterate over the list instead of using EVERY, and perhaps put everything in one single function, but this is pretty much what you need to do.