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.)

Ribosome

could these help? hackage.haskell.org/packages/archive/equivalence/0.2.3/doc/html/… and hackage.haskell.org/packages/archive/equivalence/0.2.2/doc/html/… – Quash

If I read correctly, all of these use IO or state transformer monads, meaning they use mutable data structures internally. While this is probably the kind of thing I'd like to do in the end, my current framework does not support this kind of pseudo-imperative code. But thanks for the link, I did not know this existed and it may be useful to me in the future. I clarified this in my post now. – Ribosome

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).

Seamanlike

I am afraid I cannot use impure code in my current environment. Regarding the map thing, I don't see how that could be applied to the standard union/find approach. At the moment, I have a simple and robust, purely functional implementation (I added it to my question) that uses maps, but I don't think that's what you had in mind. If I see this correctly, using a map the way you suggest would destroy all the advantage of the union/find structure, would it not? – Ribosome

Ah, now I finally understood what you meant by "substituting a persistent associative map". I think I'm going to try that, thanks. – Ribosome

Sorry for being obscure -- I have updated my answer to try and make things more clear. – Seamanlike