A persistent union-find data structure

ABSTRACT

The problem of disjoint sets, also known as union-find, consists in maintaining a partition of a finite set within a data structure. This structure provides two operations: a function find returning the class of an element and a function union merging two classes. An optimal and imperative solution is known since 1975. However, the imperative nature of this data structure may be a drawback when it is used in a backtracking algorithm. This paper details the implementation of a persistent union-find data structure as efficient as its imperative counterpart. To achieve this result, our solution makes heavy use of imperative features and thus it is a significant example of a data structure whose side effects are safely hidden behind a persistent interface. To strengthen this last claim, we also detail a formalization using the Coq proof assistant which shows both the correctness of our solution and its observational persistence.

REFERENCES

• 1: The Coq Proof Assistant. http://coq.inria.fr/.
• 2: The Objective Caml Programming Language. http://caml.inria.fr/.
• 3: Alfred V. Aho , John E. Hopcroft , Jeffrey Ullman, Data Structures and Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• 4: Henry G. Baker, Jr., Shallow binding in Lisp 1.5, Communications of the ACM, v.21 n.7, p.565-569, July 1978 [doi>10.1145/359545.359566]
• 5: Henry G. Baker, Shallow binding makes functional arrays fast, ACM SIGPLAN Notices, v.26 n.8, p.145-147, Aug. 1991 [doi>10.1145/122598.122614]
• 6: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 7: Tyng-Ruey Chuang, Fully persistent arrays for efficient incremental updates and voluminous reads, Symposium proceedings on 4th European symposium on programming, p.110-129, January 1992, Rennes, France
• 8: Sylvain Conchon and Evelyne Contejean. Ergo: A Decision Procedure for Program Verification. http://ergo.lri.fr/.
• 9: Sylvain Conchon and Jean-Christophe Filliâtre. Semi-Persistent Data Structures. Research Report, LRI, Université Paris Sud, 2007. http://www.lri.fr/~filliatr/publis/spds.ps.
• 10: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 11: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 12: James R. Driscoll , Neil Sarnak , Daniel D. Sleator , Robert E. Tarjan, Making data structures persistent, Journal of Computer and System Sciences, v.38 n.1, p.86-124, February 1989 [doi>10.1016/0022-0000(89)90034-2]
• 13: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 14: Chris Okasaki, Purely functional data structures, Cambridge University Press, New York, NY, 1998
• 15: Christine Paulin-Mohring, Inductive Definitions in the system Coq - Rules and Properties, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.328-345, March 16-18, 1993
• 16: Robert E. Shostak, Deciding Combinations of Theories, Journal of the ACM (JACM), v.31 n.1, p.1-12, Jan. 1984 [doi>10.1145/2422.322411]
• 17: Robert Endre Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM (JACM), v.22 n.2, p.215-225, April 1975 [doi>10.1145/321879.321884]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Algorithms, Verification

Keywords:
formal verification, persistence, union-find