ligo/vendors/UnionFind/README.md

40 lines
1.4 KiB
Markdown
Raw Permalink Normal View History

# Some implementations in OCaml of the Union/Find algorithm
All modules implementing Union/Find can be coerced by the same
signature `Partition.S`.
Note the function `alias` which is equivalent to `equiv`, but not
symmetric: `alias x y` means that `x` is an alias of `y`, which
translates in the present context as `x` not being the representative
of the equivalence class containing the equivalence between `x` and
`y`. The function `alias` is useful when managing aliases during the
static analyses of programming languages, so the representatives of
the classes are always the original object.
The module `PartitionMain` tests each with the same equivalence
relations.
## `Partition0.ml`
This is a naive, persistent implementation of Union/Find featuring an
asymptotic worst case cost of O(n^2).
## `Partition1.ml`
This is a persistent implementation of Union/Find with height-balanced
forests and without path compression, featuring an asymptotic worst
case cost of O(n*log(n)).
## `Partition2.ml`
This is an alternate version of `Partition1.ml`, using a different
data type.
## `Partition3.ml`
This is a destructive implementation of Union/Find with
height-balanced forests but without path compression, featuring an
asymptotic worst case of O(n*log(n)). In practice, though, this
implementation should be faster than the previous ones, due to a
smaller multiplicative constant term.