可逆本原置换的精益证明算法及相关性质
Certifying algorithms and relevant properties of Reversible Primitive Permutations with Lean
摘要：
可逆原始排列（RPP）是递归定义的函数，旨在模拟可逆计算。我们说明了一个证明，完全开发的证明助理精益，证明：“RPP可以编码每一个原始递归函数”。我们对该声明的原始证明的修改在概念上更简单，修复了一些错误，提出了一个新的更原始的RPP可逆迭代方案，并且为了保持形式化和半自动证明的简单性，我们确定了一个可以在RPP中生成一些有用的可逆算法的模式：Cantor配对，整数除法的商/提醒，截断平方根。我们的精益源代码可用于可逆计算的实验，其属性可以被认证。
英文摘要：
Reversible Primitive Permutations (RPP) are recursively defined functions designed to model Reversible Computation. We illustrate a proof, fully developed with the proof-assistant Lean, certifying that: "RPP can encode every Primitive Recursive Function". Our reworking of the original proof of that statement is conceptually simpler, fixes some bugs, suggests a new more primitive reversible iteration scheme for RPP, and, in order to keep formalization and semi-automatic proofs simple, led us to identify a single pattern that can generate some useful reversible algorithms in RPP: Cantor Pairing, Quotient/Reminder of integer division, truncated Square Root. Our Lean source code is available for experiments on Reversible Computation whose properties can be certified.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
