一句话：提出描述列表长度的子语言，支持倍增与指数增长，并给出在可预测域上完备的长度检查算法，经范畴论拉回证明终止。
许多程序以各种顺序或分治递归模式处理列表，其正确性与完备性推理需要推理列表长度，而通用长度推理通常不可判定，甚至 NP 完全。本文引入一个相对简单、并非完全通用但能覆盖大量此类模式的列表长度表达式子语言，支持倍增以及指数（迭代倍增）。作者为该子语言设计了简单的长度检查算法，并在一个可预测的问题域上证明其完备性。终止性证明通过范畴论拉回给出，并在 Agda 中形式化；同时提供 Rocq 实现，以及带 Haskell 解释器的玩具语言 Fulbourn。
Many programs process lists by recursing in a wide variety of sequential and/or divide-and-conquer patterns. Reasoning about the correctness and completeness of these programs requires reasoning about the lengths of the lists, techniques for which are typically undecidable or at least NP-complete. In this paper we show how introducing a relatively simple (sub-)language for expressions describing list lengths, whilst not completely general, covers a great number of these patterns. It includes not only doubling but also exponentiation (iterated doubling), and moreover admits a simple length-checking algorithm that is complete over a predictable problem domain. We prove termination of the algorithm via category-theoretic pullbacks, formalized in Agda, as well as providing a more realistic implementation in Rocq, and a toy language Fulbourn with interpreter in Haskell.