License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.5
URN: urn:nbn:de:0030-drops-110609
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11060/
Go to the corresponding LIPIcs Volume Portal

Affeldt, Reynald ; Garrigue, Jacques ; Qi, Xuanrui ; Tanaka, Kazunari

Proving Tree Algorithms for Succinct Data Structures

pdf-format:
LIPIcs-ITP-2019-5.pdf (0.5 MB)

Abstract

Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.

BibTeX - Entry

@InProceedings{affeldt_et_al:LIPIcs:2019:11060,
  author =	{Reynald Affeldt and Jacques Garrigue and Xuanrui Qi and Kazunari Tanaka},
  title =	{{Proving Tree Algorithms for Succinct Data Structures}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11060},
  URN =		{urn:nbn:de:0030-drops-110609},
  doi =		{10.4230/LIPIcs.ITP.2019.5},
  annote =	{Keywords: Coq, small-scale reflection, succinct data structures, LOUDS, bit vectors, self balancing trees}
}

Keywords: Coq, small-scale reflection, succinct data structures, LOUDS, bit vectors, self balancing trees
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: The accompanying Coq development can be found on GitHub (see [Reynald Affeldt et al., 2018]).

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI