- 【Updated on May 12, 2025】 Integration of CiNii Dissertations and CiNii Books into CiNii Research
- Trial version of CiNii Research Knowledge Graph Search feature is available on CiNii Labs
- Suspension and deletion of data provided by Nikkei BP
- Regarding the recording of “Research Data” and “Evidence Data”
Description
Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely one 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.
Accepted to the 10th International Conference on Interactive Theorem Proving (ITP 2019)
- Tweet
Keywords
- FOS: Computer and information sciences
- small-scale reflection
- Computer Science - Programming Languages
- D.2.4
- 005
- self balancing trees
- 004
- succinct data structures
- Computer Science - Data Structures and Algorithms
- Coq
- bit vectors
- F.3.1; E.1; D.2.4
- Data Structures and Algorithms (cs.DS)
- LOUDS
- F.3.1
- E.1
- Programming Languages (cs.PL)
Details 詳細情報について
-
- CRID
- 1871146592859373312
-
- Data Source
-
- OpenAIRE
