Semi-persistent Data Structures
A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called semi-persistence, where only ancestors of the most recent version can b
- PDF / 535,635 Bytes
- 15 Pages / 430 x 660 pts Page_size
- 19 Downloads / 211 Views
Abstract. A data structure is said to be persistent when any update operation returns a new structure without altering the old version. This paper introduces a new notion of persistence, called semi-persistence, where only ancestors of the most recent version can be accessed or updated. Making a data structure semi-persistent may improve its time and space complexity. This is of particular interest in backtracking algorithms manipulating persistent data structures, where this property is usually satisfied. We propose a proof system to statically check the valid use of semi-persistent data structures. It requires a few annotations from the user and then generates proof obligations that are automatically discharged by a dedicated decision procedure.
1
Introduction
A data structure is said to be persistent when any update operation returns a new structure without altering the old version. In purely applicative programming, data structures are automatically persistent [16]. Yet this notion is more general and the exact meaning of persistent is observationally immutable. Driscoll et al. even proposed systematic techniques to make imperative data structures persistent [9]. In particular, they distinguish partial persistence, where all versions can be accessed but only the newest can be updated, from full persistence where any version can be accessed or updated. In this paper, we study another notion of persistence, which we call semi-persistence. One of the main interests of a persistent data structure shows up when it is used within a backtracking algorithm. Indeed, when we are back from a branch, there is no need to undo the modifications performed on the data structure: we simply use the old version, which persisted, and start a new branch. One can immediately notice that full persistence is not needed in this case, since we are reusing ancestors of the current version, but never siblings (in the sense of another version obtained from a common ancestor). We shall call semi-persistent a data structure where only ancestors of the newest version can be updated. Note that this notion is different from partial persistence, since we need to update ancestors, and not only to access them. A semi-persistent data structure can be more efficient than its fully persistent counterpart, both in time and space. An algorithm using a semi-persistent data structure may be written as if it was operating on a fully persistent data structure, provided that we only backtrack to ancestor versions. Checking the S. Drossopoulou (Ed.): ESOP 2008, LNCS 4960, pp. 322–336, 2008. c Springer-Verlag Berlin Heidelberg 2008
Semi-persistent Data Structures
323
correctness of a program involving a semi-persistent data structure amounts to showing that – first, the data structure is correctly used ; – second, the data structure is correctly implemented. This article only addresses the former point. Regarding the latter, we simply give examples of semi-persistent data structures. Proving the correctness of these implementations is out of the scope of th
Data Loading...
