Lookup tables (finite maps) are a ubiquitous data structure. In pure functional languages they are best represented using trees instead of hash tables. In pure functional languages within constructive logic, without a primitive integer type, they are well represented using binary tries instead of search trees. In this work, we introduce canonical binary tries, an improved binary-trie data structure that enjoys a natural extensionality property, quite useful in proofs, and supports sparseness more efficiently. We provide full proofs of correctness in Coq. We provide microbenchmark measurements of canonical binary tries versus several other data structures for finite maps, in a variety of application contexts; as well as measurement of canonical versus original tries in a big, real system. The application context of data structures contained in theorem statements imposes unusual requirements for which canonical tries are particularly well suited.

翻译：查找表格( 无限地图) 是无处不在的数据结构。 在纯功能语言中, 他们最能代表的是树木而不是散列表格。 在建设性逻辑范围内的纯功能语言中, 没有原始整数类型, 他们完全能代表的是二进制尝试, 而不是搜索树。 在这项工作中, 我们引入了粗体二进制尝试, 改进的二进制数据结构, 具有自然延伸性属性, 在证明中非常有用, 并更高效地支持稀疏性 。 我们在 Coq 中提供了完整的正确性证据 。 我们提供了在各种应用背景下对定点地图的卡通性二进制尝试和若干其他数据结构的微比目标记测量 ; 以及在大型、 真实系统中的卡通式尝试和原始尝试的测量 。 语标中包含的数据结构的应用背景提出了不寻常的要求, 而 语法性尝试特别适合 。