Äquivalenzklassen und Vereinigung/Finden in einer funktionalen Sprache

Question

Für einen Automatenalgorithmus benötige ich eine schnelle Union-Find-Datenstruktur in einer funktionalen Sprache. Da ich die Korrektheit der Datenstruktur formal nachweisen muss, würde ich eine einfache Struktur bevorzugen.

Was ich versuche zu tun, ist die Äquivalenzklassen der Elemente in einer Menge S w.r.t zu berechnen. eine Beziehung R ⊆ S × S. Was ich am Ende herausbekommen möchte, ist eine Funktion f: S → S, die jedes Element von S einem (kanonischen) Vertreter seiner R -Äquivalenzklasse zuordnet. Mit "kanonisch" meine ich, dass es mir egal ist, welcher Repräsentant es ist, solange es für alle Elemente einer Äquivalenzklasse gleich ist, d. H. Ich möchte f x = f y ⟺ (x,y) ∈ R halten.

Was wäre die beste Datenstruktur und Algorithmus dafür in einer funktionalen Sprache? Ich sollte hinzufügen, dass ich wirklich "normalen" Funktionscode benötige, d. H. Keine Wandlungs-/Zustandstransformator-Monaden.

EDIT: In der Zwischenzeit habe ich mit diesem Algorithmus kommen:

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] 

Diese Karte, die jedes Element von S ihrer Äquivalenzklasse an den Vertreter abbildet schafft, wo der Vertreter ist der erste Element, das durch die Iteration über S erreicht wird. Ich denke, das hat tatsächlich lineare Zeit (wenn Kartenoperationen konstant sind). Ich bin jedoch immer noch an anderen Lösungen interessiert, da ich nicht weiß, wie effizient das in der Praxis ist.

(meine Beziehung intern als "S → (S Set) Option" dargestellt wird, damit die Iteration über. {T | (s, t) ∈ R} - das ist ein billiger Betrieb auf dieser Struktur)

Answer 1

AFAIK (und eine Schnellsuche hat mich nicht entmannt), es ist kein rein funktionelles Äquivalent zum herkömmlichen disjoint-set datastructure bekannt, das eine vergleichbare asymptotische Leistung aufweist (Amortisierte Inverse-Ackermann-Funktion). (Die herkömmliche Datenstruktur ist nicht rein funktional, da sie eine destruktive Aktualisierung zur Pfadkomprimierung erfordert)

Wenn Sie nicht auf funktionale Reinheit eingestellt sind, können Sie einfach die destruktive Aktualisierung verwenden und die konventionelle Datenstruktur implementieren.

Wenn Sie die asymptotische Leistung nicht anpassen möchten, können Sie das Random-Access-Array der konventionellen Datenstruktur durch persistent associative map ersetzen, auf Kosten eines zusätzlichen O (log N) -Leistungsfaktors, und müssen es überprüfen Richtigkeit.

Wenn Sie maximale Einfachheit für Verifikationszwecke wünschen und auf keinem der oben genannten Punkte nicht gesetzt sind, können Sie ein updatebares Array und die gewerksweise Optimierung verwenden. IIRC dies ergibt O (log N) amortisierte Worst-Case-Leistung, kann aber tatsächlich die praktische Ausführungsgeschwindigkeit verbessern (da der Rang nicht mehr gespeichert oder verwaltet werden muss).