Notes on the Nested Sets


Introduction

When I presented the set library at the ACL2 meeting on February 11, 2004, a great deal of confusion ensued as to whether or not nested sets were supported by the library. My answer is and was a firm yes, but several factors and misunderstandings seemed to arise. On this page, I present a more thorough overview of exactly in what sense nested sets are supported, and deal with some of the issues that were causing confusion.

Thanks to J Strother Moore and Robert Krug for insightful commentary regarding the issues here!

Nested Sets in the Standard Library

In the standard sets library, lists within a set are considered to be sets. For example, we can see that the cardinality of the following set is considered to be 1, because the lists are compared using set equality (S::=).

(S::cardinality '( (1 2) (2 1) )) = 1

If you want to have a set of lists in the standard library, you must explicitly tag your lists with the special symbol :UR-CONS. This is done so that the set functions will know which equality operation to use (set equality S::= or element equality equal).

As an example, if you wanted to represent the set containing the lists (1 2 3) and (3 2 1) in the standard sets library, you might do this:

  (let ((x '(:UR-CONS (1 2 3)))       ; x = (1 2 3)
        (y '(:UR-CONS (3 2 1))))      ; y = (3 2 1)
       (S::scons x (S::scons y nil)))

This produces a set with explicitly tagged list elements:

((:UR-CONS (1 2 3)) (:UR-CONS (3 2 1)))

The :UR-CONS tags instruct the set functions to use equal to compare the values of these elements, rather than S::= which would do a comparison based on double-containment.

As a general rule:

Nested Sets in the Ordered Library

In the ordered sets library, set equality and element equality are the same thing, namely the equal function. As a result, and in direct contrast to the standard sets library, lists within a set are considered to be lists, not sets. For example, we can see that the cardinality of the following set is considered to be 2, because this is considered to be a set of two distinct lists.

(SETS::cardinality '( (1 2) (2 1) )) = 2

How, then, are nested sets supported? It is actually very simple, because sets are just ordinary ACL2 objects, and set equality is just equal. If you want a set of sets, just insert sets into a new set.

As an example, consider set S below, given in a traditional math notation and with repeated elements. These curly braces are intended to mean sets, and not lists.

S = { {{1, 2}, {2, 1}}, 
      {{2, 1}, {1, 2}} }

We can create this set as follows:

    (let* ((x (insert 1 (insert 2 nil)))    ; x = {1, 2}
           (y (insert 2 (insert 1 nil)))    ; y = {2, 1}
           (A (insert x (insert y nil)))    ; A = { {1, 2}, {2, 1} }
           (B (insert y (insert x nil))))   ; B = { {2, 1}, {1, 2} }
        (insert A (insert B nil)))

If you evaluate this expression in ACL2, the answer is (((1 2))). And really this is exactly what should be expected, because S is exactly {{{1,2}}} after you remove the duplicate elements.

As a general rule:

Mixing Sets and Lists

An objection was raised that the ordered sets library would be unable to represent the set containing as its elements: the set {1, 2}, and the list (1 2). The issue here is that the set {1, 2} and the list (1 2) have exactly the same representation in the ordered library, and so if you do the following:

(insert (list 1 2) 
  (insert (insert 1 (insert 2 nil))
    nil))

Then the result is the ACL2 object ((1 2)). This set behaves as we would expect with respect to membership, for example (list 1 2) is a member, and (insert 1 (insert 2 nil)) is also a member. However, its cardinality is 1 instead of 2.

In contrast, the standard sets library might represent this set as ((:UR-CONS (1 2)) (1 2)), which has the expected membership property: (1 2), the set, is a member, as is (:UR-CONS (1 2)), the representation for the list (1 2). Furthermore, the cardinality of this set is 2, and so there is clear support for being able to have sets which mix sets and lists as elements.

The difference here is that by tagging non-sets, the standard sets library is able to distinguish between sets and lists. In the ordered sets library, this distinction does not exist, because the representation of sets and lists is exactly the same.

A Solution For Mixing Sets and Lists

Suppose that in the ordered sets library, you wanted to treat sets as "first class objects" which are different than lists. In other words, you want to be able to mix sets and lists as elements of a set, and differentiate between them even though their representations might be the same.

Then, a solution is to tag the non-set lists, just as you would in the standard sets library. Note that the actual tag used is not important, so long as you are consistent. For example:

(insert (list :FOO '(1 2))
  (insert (insert 1 (insert 2 nil))
    nil))

Now we can say that (1 2), the set {1, 2} is a member of this set, as is our representation of the list (1 2), namely (:FOO (1 2)). Also, the cardinality of this set is 2, as we would hope. Note also that lists containing the element :FOO can be supported, e.g. the representation for (:FOO (1 2)) is (:FOO (:FOO (1 2))).

This is more or less the same approach taken by the standard sets library's tag :UR-CONS. However, in the standard library, this tag is used in order to determine which equality test should be performed on the set elements. Since there is only one notion of equality in the ordered sets world, there is no need to directly support any one tag within the library.