可连接红黑树的经过验证的代价分析

以连接(join)操作组合序列的有序数据序列，是并行函数式算法实现的基础。这种抽象数据类型可以使用平衡二叉树优雅且高效地实现，其中提供连接操作以合并两棵树并在必要时重新平衡。在这项工作中，我们提出了在用于代价分析的依赖类型论 $\textbf{calf}$ 中可连接红黑树的经过验证的实现与代价分析。我们以所有正确性不变量均被内在维持的方式实现红黑树及辅助中间数据结构。然后，我们利用红黑树不变量描述并验证了操作的精确代价界。最后，我们使用基于简单连接的接口实现序列上的标准算法，并在以红黑树作为底层实现的情况下界定其代价。所有证明均通过使用 $\textbf{calf}$ 在 Agda 定理证明器中的嵌入形式化机械化。