简洁数据结构的证明树算法
Proving tree algorithms for succinct data structures
摘要：
简洁的数据结构可以在不牺牲性能的情况下高效地表示大量数据。他们依靠一个巧妙设计的数据表示和算法。我们在这里提出的形式化Coq/SSReflect的两个不同的基于树的简洁表示和他们的配套算法。一种是Level-Order Unary Degree Sequence，它将树的结构以宽度优先顺序编码为比特序列，其中访问操作可以根据Rank和Select来定义，对于静态比特序列，它们在恒定时间内工作。另一种将动态位序列表示为二进制平衡树，其中Rank和Select与其静态版本相比呈现低对数开销，并且具有有效的插入和删除。例如，这两者可以堆叠以提供字典的动态表示。虽然这两种表示都是众所周知的，但我们相信这是它们的第一次形式化，也是实现可证明安全的大数据所需的一步。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
