发表机构
Johannes Kepler University; Université de Lorraine（约翰内斯·开普勒大学; 洛林大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究对特定Patience Sort算法的递归优化过程进行形式化认证，对比Theorema与Rocq框架的实现差异，揭示算法设计对形式证明复杂度的影响。
AI 中文摘要
本案例研究针对特定版本的Patience Sort（耐心排序）算法，展示了其从直观但低效的嵌套递归，演变为更复杂但更高效的尾递归的过程，并介绍了该算法在Theorema和Rocq（前称Coq）中的形式化实现与认证。我们归纳了算法转换的若干通用原则，构建了所需的基础理论与证明方法。一项显著特色是，Theorema中的方法采用多重集，简化了整个流程且更具直观性。认证过程凸显了Theorema与Rocq方法间的显著差异，我们从算法定义、证明开发与证明工作量三个维度展开对比分析。该分析揭示了算法设计如何影响形式证明的复杂度与结构，同时证明了非平凡算法可在不同形式化框架中得到有效验证。
英文摘要
This is a case study on a specific version of the Patience Sort algorithm in which we illustrate the evolution of it from an intuitive but inefficient nested recursion into a more complex but more efficient tail recursion, together with its formal implementation and certification in Theorema and Rocq (formerly Coq). We identify some general principles of algorithm transformation, and we develop the necessary background theory and proof methods. As a significant distinctive aspect, the approach in Theorema uses multisets, which simplifies the whole process and makes it more intuitive. The certification process reveals significant differences between the Theorema and Rocq approaches, about which we provide a comparative analysis with respect to algorithm definition, proof development, and proof effort. This analysis offers insights into how algorithm design influences the complexity and structure of formal proofs and demonstrates how non-trivial algorithms can be effectively verified across different formal frameworks.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 138-157
