一句话：为有限列表上的龟兔算法给出组合式解释，并用 OCaml 与 Coq 形式化验证回文检测器。
论文关注在不可变有限列表上实现龟兔（快慢指针）算法的组合式理解。传统上，快指针到达表尾时慢指针指向中间的属性可支持一次递归遍历、最少比较次数的回文检测，常以 TABA 递归模式实现。本文在 OCaml 中重构该回文检测器，并用 Coq 证明助手形式化并证明其正确性。更一般地，作者说明使用快慢指针的程序可以表示为普通列表 fold，并可通过列表上的普通结构归纳进行推理，从而获得组合式解释。文章还给出 TABA 递归模式及其尾递归变体 There And Forth Again 的十余个新应用。
In the tortoise-and-hare algorithm, when the fast pointer reaches the end of a finite list, the slow pointer points to the middle of this list. In the early 2000’s, this property was found to make it possible to program a palindrome detector for immutable lists that operates in one recursive traversal of the given list and performs the smallest possible number of comparisons, using the “There And Back Again” (TABA) recursion pattern. In this article, this palindrome detector is reconstructed in OCaml, formalized with the Coq Proof Assistant, and proved to be correct. More broadly, this article presents a compositional account of the tortoise-and-hare algorithm for finite lists. Concretely, compositionality means that programs that use a fast and a slow pointer can be expressed with an ordinary fold function for lists and reasoned about using ordinary structural induction on the given list. This article also contains a dozen new applications of the TABA recursion pattern and of its tail-recursive variant, “There and Forth Again”.
@article{paperbot2141,
title = {The Tortoise and the Hare Algorithm for Finite Lists, Compositionally},
author = {Olivier Danvy},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {1},
year = {2023},
doi = {10.1145/3564619}
}