一句话：提出与命令式版本同速的 move-to-root、splay、zip 树函数式算法，并在 Coq/Iris 中机器验证等价性。
重平衡二叉搜索树算法通常以命令式伪代码给出，因为其性能依赖原地更新而非反复分配新节点，但这也使验证困难：循环不变式必须关联正在重平衡的未完成树片段。本文为 move-to-root、splay 和 zip 树提出新的函数式访问与插入算法，性能与命令式版本相当，正确性却可通过简单归纳论证建立。对每种结构，作者给出基于 zipper 的自底向上算法，以及使用新的一等构造子上下文原语的自顶向下算法。函数式与命令式算法等价，并在 Coq 的 Iris 框架中机器化验证，从而得到已知二叉搜索树算法的首个完全验证实现，性能与最快的 C 实现相当。
Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.
@article{LorenzenLSL24,
title = {The Functional Essence of Imperative Binary Search Trees},
author = {Anton Lorenzen and Daan Leijen and Wouter Swierstra and Sam Lindley},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656398}
}