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!

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:

- If you want X to be a set of sets, then insert sets/lists into X.
- If you want X to be a set of lists, then prepend your lists with :UR-CONS.

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:

- If you want X to be a set of sets, then insert sets into X.
- If you want X to be a set of lists, then insert lists into X.

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.

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.