Certifying expressive power and algorithms of reversible primitive permutations with Lean

Reversible primitive permutations (RPP) is a class of recursive functions that models reversible computation. We present a proof, which has been verified using the proof-assistant Lean, that demonstrates RPP can encode every primitive recursive function (PRF-completeness) and that each RPP can be encoded as a primitive recursive function (PRF-soundness). Our proof of PRF-completeness is simpler and fixes some errors in the original proof, while also introducing a new reversible iteration scheme for RPP. By keeping the formalization and semi-automatic proofs simple, we are able to identify a single programming pattern that can generate a set of reversible algorithms within RPP: Cantor pairing, integer division quotient/remainder, and truncated square root. Finally, Lean source code is available for experiments on reversible computation whose properties can be certified.

Automated summary

In this article, reversible primitive permutations (RPP) are introduced as a class of recursive functions that model reversible computation. The authors present a proof, verified using the proof-assistant Lean, demonstrating that RPP can encode every primitive recursive function and that each RPP can be encoded as a primitive recursive function. The article also highlights a programming pattern for reversible algorithms and provides Lean source code for experimentations with certified properties of reversible computation.