		Search-engine friendly clone of the ACL2 documentation.

Deflist

Strict-list-recognizers

Should your list recognizers require nil-terminated lists?

Here are two ways that you could write a list recognizer:

The "strict" way:

(defun foo-listp (x)
  (if (atom x)
      (not x)
    (and (foop (car x))
         (foo-listp (cdr x)))))

The "loose" way:

(defun foo-listp (x)
  (if (atom x)
      t
    (and (foop (car x))
         (foo-listp (cdr x)))))

The only difference is that in the base case, the strict recognizer requires X to be NIL, whereas the loose recognizer allows X to be any atom.

By default, the recognizers introduced by deflist follow the loose approach. You can use the :true-listp option to change this behavior, and instead introduce a strict recognizer.

Why in the world would we use a loose recognizer? Well, there are advantages to either approach.

The strict approach is certainly more clear and less weird. It is nice that a strict recognizer always implies true-listp. And it makes EQUAL more meaningful when applied to FOO-LISTP objects.

That is, when FOO-LISTP is strict, there is only one FOO-LISTP that has length 3 and whose first three elements are (A B C). However, when FOO-LISTP is loose, there are infinitely many lists like this, and the only difference between them is their final cdr.

This nicer equality behavior makes the strict approach especially appealing when you are building new data types that include FOO-LISTP components, and you'd like to just reuse EQUAL instead of having new equivalence relations for each structure.

But the loose approach more nicely follows the list-fix convention: "a function that takes a list as an argument should coerce the final-cdr to NIL, and produce the same result regardless of the final cdr." More formally, you might say that F respects the list-fix convention when you can prove

(defcong list-equiv equal (f ... x ...) n)

Where list-equiv is equality up to the final cdr, e.g.,

(list-equiv x y) = (equal (list-fix x) (list-fix y))

Many functions follow this convention or something similar to it, and because of this there are sometimes nicer theorems about loose list recognizers than about strict list recognizers. For instance, consider append. In the loose style, we can prove:

(equal (foo-listp (append x y))
       (and (foo-listp x)
            (foo-listp y)))

In the strict style, we have to prove something uglier, e.g.,

(equal (foo-listp (append x y))
       (and (foo-listp (list-fix x))
            (foo-listp y)))

There are many other nice theorems, but just as a few examples, each of these theorems are very nice in the loose style, and are uglier in the strict style:

(equal (foo-listp (list-fix x))
       (foo-listp x))

(equal (foo-listp (rev x))
       (foo-listp x))

(equal (foo-listp (mergesort x))
       (foo-listp x))

(implies (and (subsetp-equal x y)
              (foo-listp y))
         (foo-listp x))

deflist originally came out of ACL2::milawa, where I universally applied the loose approach, and in that context I think it is very nice. It's not entirely clear that loose recognizers are a good fit for ACL2. Really one of the main objections to the loose style is: ACL2's built-in list recognizers use the strict approach, and it can become irritating to keep track of which recognizers require true-listp and which don't.