Journal
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
Volume 136, Issue -, Pages -Publisher
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jlamp.2023.100923
Keywords
Reversible computation; Primitive recursion; Lean
Categories
Ask authors/readers for more resources
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.
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available