Document Open Access Logo

Proving Tree Algorithms for Succinct Data Structures

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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.5.pdf
  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Author Details

Reynald Affeldt
  • National Institute of Advanced Industrial Science and Technology, Tsukuba, Japan
Jacques Garrigue
  • Graduate School of Mathematics, Nagoya University, Japan
Xuanrui Qi
  • Department of Computer Science, Tufts University, Medford, MA, United States
Kazunari Tanaka
  • Graduate School of Mathematics, Nagoya University, Japan

Acknowledgements

We acknowledge the support of the JSPS-CNRS bilateral program "FoRmal tools for IoT sEcurity" and the JSPS KAKENHI Grant Number 18H03204, thank the projects' participants, in particular Akira Tanaka for his comments on code extraction, and the anonymous reviewers for their comments that helped improve this paper.

Cite AsGet BibTex

Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Proving Tree Algorithms for Succinct Data Structures. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.5

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Data structures design and analysis
  • Software and its engineering → Formal software verification
Keywords
  • Coq
  • small-scale reflection
  • succinct data structures
  • LOUDS
  • bit vectors
  • self balancing trees

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

  • The accompanying Coq development can be found on GitHub (see [Reynald Affeldt et al., 2018]).

References

  1. Stephen Adams. Functional Pearls: Efficient sets - a balancing act. Journal of Functional Programming, 3(4):553-561, October 1993. Google Scholar
  2. G. M. Adel’son-Vel’skĭı and E. M. Landis. An algorithm for the organization of information. Soviet Mathematics-Doklady, 3(5):1259-1263, September 1962. Google Scholar
  3. Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. A Coq formalization of succinct data structures. https://github.com/affeldt-aist/succinct, 2018.
  4. Andrew W. Appel. Efficient Verified Red-Black Trees. Available at http://www.cs.princeton.edu/~appel/papers/redblack.pdf (code included in Coq standard library, file MSetRBT.v, with extra modifications by Pierre Letouzey), September 2011.
  5. Adam Chlipala. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013. Google Scholar
  6. Jean-Christophe Filliâtre and Pierre Letouzey. Functors for Proofs and Programs. In Proceedings of the 13th European Symposium on Programming (ESOP 2004), Barcelona, Spain, March 29-April 2, 2004, volume 2986 of Lecture Notes in Computer Science, pages 370-384. Springer, 2004. Source code about red-black trees available at URL: https://github.com/coq-contribs/fsets/SetRBT.v.
  7. Jeremy Gibbons. Algebras for Tree Algorithms. PhD thesis, Programming Research Group, Oxford University, 1991. Available as Technical Monograph PRG-94. Google Scholar
  8. Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A Small Scale Reflection Extension for the Coq system. Technical report, INRIA, 2008. Version 17 (Nov 2016). Google Scholar
  9. Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. Journal of Functional Programming, 23(4):357–401, 2013. Google Scholar
  10. Geraint Jones and Jeremy Gibbons. Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips. Technical Report 71, Department of Computer Science, University of Auckland, 1993. Google Scholar
  11. Stefan Kahrs. Red-black trees with types. Journal of Functional Programming, 11(4):425-432, July 2001. Google Scholar
  12. Taku Kudo, Toshiyuki Hanaoka, Jun Mukai, Yusuke Tabata, and Hiroyuki Komatsu. Efficient dictionary and language model compression for input method editors. In Proceedings of the Workshop on Advances in Text Input Methods (WTIM 2011), pages 19-25, 2011. Google Scholar
  13. Dominique Larchey-Wendling and Ralph Matthes. Certification of Breadth-First Algorithms by Extraction. In Proceedings of the 13th International Conference on Mathematics of Program Construction, 2019. Google Scholar
  14. Assia Mahboubi and Enrico Tassi. Mathematical Components. Available at: https://math-comp.github.io/mcb/, 2016. With contributions by Yves Bertot and Georges Gonthier.
  15. Gonzalo Navarro. Compact Data Structures: A Practical Approach. Cambridge University Press, 2016. Google Scholar
  16. Gonzalo Navarro and Kunihiko Sadakane. Fully Functional Static and Dynamic Succinct Trees. ACM Transactions on Algorithms, 10(3), 2014. Google Scholar
  17. Tobias Nipkow. Automatic Functional Correctness Proofs for Functional Search Trees. In Interactive Theorem Proving (ITP 2016), volume 9807 of Lecture Notes in Computer Science, pages 307-322. Springer, 2016. Google Scholar
  18. Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. Google Scholar
  19. Julien Oster. An Agda implementation of deletion in Left-leaning Red-Black trees. Available at https://www.reinference.net/llrb-delete-julien-oster.pdf, March 2011.
  20. Rajeev Raman, Venkatesh Raman, and S. Srinivasa Rao. Succinct Dynamic Data Structures. In Proceedings of the 7th International Workshop on Algorithms and Data Structures, pages 426-437. Springer, 2001. Google Scholar
  21. Ilya Sergey. Programs and Proofs: Mechanizing Mathematics with Dependent Types (Lecture Notes). Available at URL: https://ilyasergey.net/pnp/.
  22. Ilya Sergey and Aleksandar Nanevski. Introducing Functional Programmers to Interactive Theorem Proving and Program Verification (Teaching Experience Report). Available at https://ilyasergey.net/papers/teaching-ssr.pdf, 2015.
  23. Matthieu Sozeau. Un environnement pour la programmation avec types dépendants. PhD thesis, Université de Paris-Sud, 2008. Google Scholar
  24. Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. Formal Verification of the rank Algorithm for Succinct Data Structures. In 18th International Conference on Formal Engineering Methods (ICFEM 2016), Tokyo, Japan, November 14-18, 2016, volume 10009 of Lecture Notes in Computer Science, pages 243-260. Springer, November 2016. Google Scholar
  25. Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. Safe Low-level Code Generation in Coq using Monomorphization and Monadification. Journal of Information Processing, 26:54-72, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact