A persistent union-find data structure

Sylvain Conchon; Jean Christophe Filliâtre

doi:10.1145/1292535.1292541

A persistent union-find data structure

Sylvain Conchon, Jean Christophe Filliâtre

INRIA Saclay, Laboratoire de Recherche en Informatique (LRI), Université Paris Sud

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	ML'07
Subtitle of host publication	Proceedings of the 2007 Workshop on ML
Pages	37-46
Number of pages	10
DOIs	https://doi.org/10.1145/1292535.1292541
Publication status	Published - 1 Dec 2007
Externally published	Yes
Event	ML'07: 2007 Workshop on ML - Freiburg, Germany Duration: 5 Oct 2007 → 5 Oct 2007

Publication series

Name	ML'07: Proceedings of the 2007 Workshop on ML

Conference

Conference	ML'07: 2007 Workshop on ML
Country/Territory	Germany
City	Freiburg
Period	5/10/07 → 5/10/07

Keywords

Formal verification
Persistence
Union-find

Access to Document

10.1145/1292535.1292541

Cite this

@inproceedings{5443399f152f4a7c884c2fb0a15ff6a2,

title = "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.",

keywords = "Formal verification, Persistence, Union-find",

author = "Sylvain Conchon and Filli{\^a}tre, \{Jean Christophe\}",

year = "2007",

month = dec,

day = "1",

doi = "10.1145/1292535.1292541",

language = "English",

isbn = "9781595936769",

series = "ML'07: Proceedings of the 2007 Workshop on ML",

pages = "37--46",

booktitle = "ML'07",

note = "ML'07: 2007 Workshop on ML ; Conference date: 05-10-2007 Through 05-10-2007",

}

TY - GEN

T1 - A persistent union-find data structure

AU - Conchon, Sylvain

AU - Filliâtre, Jean Christophe

PY - 2007/12/1

Y1 - 2007/12/1

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

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

KW - Formal verification

KW - Persistence

KW - Union-find

U2 - 10.1145/1292535.1292541

DO - 10.1145/1292535.1292541

M3 - Conference contribution

AN - SCOPUS:38849112459

SN - 9781595936769

T3 - ML'07: Proceedings of the 2007 Workshop on ML

SP - 37

EP - 46

BT - ML'07

T2 - ML'07: 2007 Workshop on ML

Y2 - 5 October 2007 through 5 October 2007

ER -

A persistent union-find data structure

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this