		Search-engine friendly clone of the ACL2 documentation.

Std/osets

In

(in a x) determines if a is a member of the set X.

The logical definition of in makes no mention of the set order, except implicitly by the use of the set primitives like head and tail.

The :exec version just inlines the set primitives and does one level of loop unrolling. On CCL, it seems to run about 2.6x faster on the following loop:

;; 4.703 sec logic, 1.811 sec exec
(let ((big-set (loop for i from 1 to 100000 collect i)))
  (gc$)
  (time (loop for i fixnum from 1 to 30000 do (set::in i big-set))))

There are other ways we could optimize in. Since the set is ordered, we could try to use the set order << to stop early when we ran into an element that is larger than the one we are looking for. For instance, when looking for 1 in the set '(2 3 4), we know that since 1 << 2 that 1 cannot be a member of this set.

The simplest way to do this is to use << at every element. But set order comparisons can be very expensive, especially when sets contain large cons structures. So while it is easy to contrive situations where exploiting the order would be advantageous, like

(in 1 '(2 3 4 .... 100000))

where we could return instantly, there are also times where it would be slower. For instance, on

(in 100001 '(1 2 3 4 ... 100000))

we would incur the extra cost of 100,000 calls to <<.

For this reason, we do not currently implement any short-circuiting. The reasoning is:

it is not clear which would be faster in all cases,
it is not clear what the typical usage behavior of in is, so even if we wanted to benchmark alternate implementations, it may be hard to come up with the right benchmarking suite
both solutions are O(n) anyway, and in isn't a function that should probably be used in any kind of loop so its performance shouldn't be especially critical to anything
the current method is arguably no less efficient than an unordered implementation.

Future note. In principle membership in an ordered list might be done in O(log_2 n). We are considering using a galloping membership check in the future to obtain something along these lines.

Definitions and Theorems

Function: in

(defun in (a x)
       (declare (xargs :guard (setp x)))
       (mbe :logic (and (not (empty x))
                        (or (equal a (head x)) (in a (tail x))))
            :exec (and x
                       (or (equal a (car x))
                           (and (cdr x)
                                (or (equal a (cadr x))
                                    (in a (cddr x))))))))

Theorem: in-type

(defthm in-type
        (or (equal (in a x) t)
            (equal (in a x) nil))
        :rule-classes :type-prescription)

Theorem: not-in-self

(defthm not-in-self (not (in x x)))

Theorem: in-sfix-cancel

(defthm in-sfix-cancel
        (equal (in a (sfix x)) (in a x)))

Theorem: never-in-empty

(defthm never-in-empty
        (implies (empty x) (not (in a x))))

Theorem: in-set

(defthm in-set (implies (in a x) (setp x)))

Theorem: in-tail

(defthm in-tail
        (implies (in a (tail x)) (in a x)))

Theorem: in-tail-or-head

(defthm in-tail-or-head
        (implies (and (in a x) (not (in a (tail x))))
                 (equal (head x) a)))

Theorem: in-head

(defthm in-head
        (equal (in (head x) x) (not (empty x))))