|
|
|---|
|
|
|
|---|
A tree-based implementation of finite sets.
This implementation of finite sets offers practically logarithmic worst-case performance for the core set operations (in, insert, delete) while also insisting on a canonical internal structure which allows equal to represent true set equivalence.
This library closely follows ACL2::std/osets. The first major difference, from an external user-perspective, is performance. Below are the practical worst-case complexities of core operations:
The other major difference is in how one iterates over or traverses a set. In ACL2::std/osets, set::head provides the minimal element of a nonempty set, and tail provides the rest. For treesets, head provides the hash-maximal element of a nonempty set. Instead of tail, we have left and right, providing two disjoint subsets with all elements less than and all elements greater than the head, respectively.
In practice, the set::head/head values are typically considered arbitrary elements of the set (and this perspective is encouraged). So the only meaningful difference is the tree-traversal with left and right in contrast to the flat list traversal of tail. Alternatively, one may use to-list to get a flat list to iterate over more easily.