Reseña: Proving tree algorithms for succinct data structures
Se ha publicado un artículo de razonamiento formalizado en Coq sobre algorítmica titulado Proving tree algorithms for succinct data structures.
Sus autores son
- Reynald Affeldt (del National Institute of Advanced Industrial Science and Technology (AIST) en Japón),
- Jacques Garrigue (de la Nagoya University en Japón),
- Xuanrui Qi (de la Tufts University en EE.UU.) y
- Kazunari Tanaka
Su resumen es
Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different succinct tree algorithms. One is the Level-Order Unary Degree Sequence (aka LOUDS), 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 red-black trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient Insert and Delete. 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.
El trabajo se ha presentado el 30 de agosto en el JSSST 2018 (The 35th Meeting of the Japan Society for Software Science and Technology).
El código de las correspondientes teorías se encuentra GitHub.