一句话：提出一种用代数与类型纪律刻画分治递归的方法，并在 Coq 中实现验证，无需结构递归或依赖类型。
本文研究如何在 Coq 中编写并验证分治递归程序。既有工作用代数方法刻画递归方案，本文将其扩展到分治递归：把递归表示为一种代数，外层递归可以启动内层递归来构造可供外层合法递归的数据。终止性完全由递归方案的类型纪律保证，且对底层类型系统要求不高，可在 System Fω 加有限形式的正递归类型中实现。Coq 实现不依赖结构递归或依赖类型。作者用归并排序、快速排序、Harper 正则表达式匹配器等例子展示方法，并导出带索引版本，实现一种可用于推理此类函数的分治归纳。
This paper proposes a new approach to writing and verifying divide-and-conquer programs in Coq. Extending the rich line of previous work on algebraic approaches to recursion schemes, we present an algebraic approach to divide-and-conquer recursion: recursions are represented as a form of algebra, and from outer recursions, one may initiate inner recursions that can construct data upon which the outer recursions may legally recurse. Termination is enforced entirely by the typing discipline of our recursion schemes. Despite this, our approach requires little from the underlying type system, and can be implemented in System F ω plus a limited form of positive-recursive types. Our implementation of the method in Coq does not rely on structural recursion or on dependent types. The method is demonstrated on several examples, including mergesort, quicksort, Harper’s regular-expression matcher, and others. An indexed version is also derived, implementing a form of divide-and-conquer induction that can be used to reason about functions defined via our method.
@article{paperbot2049,
title = {A Type-Based Approach to Divide-and-Conquer Recursion in Coq},
author = {Pedro Abreu and Benjamin Delaware and Alex Hubers and Christa Jenkins and J. Garrett Morris and Aaron Stump},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571196}
}