A Class of Reversible Primitive Recursive Functions

Reversible computing is bi-deterministic which means that its execution is both forward and backward deterministic, i.e. next/previous computational step is uniquely determined. Various approaches exist to catch its extensional or intensional aspects and properties. We present a class RPRF of reversible functions which holds at bay intensional aspects and emphasizes the extensional side of the reversible computation by following the style of Dedekind-Robinson Primitive Recursive Functions. The class RPRF is closed by inversion, can only express bijections on integers — not only natural numbers —, is expressive enough to embed Primitive Recursive Functions and, of course, its evaluation is effective.