论文标题
通过精益来证明可逆原始排列的算法和相关属性
Certifying algorithms and relevant properties of Reversible Primitive Permutations with Lean
论文作者
论文摘要
可逆的原始排列（RPP）是递归定义的函数，旨在建模可逆计算。我们说明了一个以证明辅助的精益开发的证明，并证明：“ RPP可以编码每个原始递归功能”。 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.我们的精益源代码可用于可逆计算的实验，其属性可以经过认证。
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.
