Equivalence classes and union/find in a functional language

Question

For an automata algorithm, I require a fast Union-Find data structure in a functional language. Since I need to formally prove the correctness of the data structure, I would prefer a simple structure.

What I am trying to do is to compute the equivalence classes of elements in a set S w.r.t. a relation R ⊆ S × S. What I want to get out in the end is some function f: S → S that maps any element of S to a (canonical) representative of its R-equivalence class. By "canonical", I mean that I don't care which representative it is as long as it is the same for all elements of one equivalence class, i.e. I want f x = f y ⟺ (x,y) ∈ R to hold.

What would the best data structure and algorithm for this be in a functional language? I should add that I really need "normal" functional code, i.e. no mutability/state transformer monads.

EDIT: In the mean time, I have come up with this algorithm:

m := empty map
for each s ∈ S do
  if m s = None then
    for each t in {t | (s,t) ∈ R}
      m := m[t ↦ s]

This creates a map that maps any element of S to the representative of its equivalence class, where the representative is the first element that is reached by the iteration over S. I think this actually has linear time (if map operations are constant). However, I am still interested in other solutions, since I don't know how efficient this is in practice.

(my relation is internally represented as a "S → (S Set) option", hence the iteration over {t | (s,t) ∈ R} - this is a cheap operation on that structure.)

Answer 1

AFAIK (and a quick search did not disabuse me), there is no known purely-functional equivalent of the conventional disjoint-set datastructure which has comparable asymptotic performance (amortized inverse-Ackermann-function). (the conventional datastructure is not purely-functional because it requires destructive update to perform path compression)

If you are not dead-set on functional purity, you can just use destructive update, and implement the conventional datastructure.

If you don't care about matching asymptotic performance, you can replace the random access array of the conventional datastructure with a persistent associative map, at the expense of an additional O(log N) performance factor, and of needing to verify its correctness.

If you want maximum simplicity for verification purposes, and aren't dead-set on either of the above, you can use an updateable array and drop the union-by-rank optimization. IIRC this yields O(log N) amortized worst-case performance, but may actually improve practical execution speed (as the rank no longer needs to be stored or managed).