Algorithmically Expressive, Always-Terminating Model for Reversible Computation

Concerning classical computational models able to express all the Primitive Recursive Functions (PRF), there are interesting results regarding limits on their algorithmic expressiveness, meant as the possibility to naturally express algorithms with minimal computational cost. By introducing the reversible computational model \(\textsf{For}_{\textsf{est}}\) , to our knowledge, we provide a first study of analogous properties, adapted to the context of reversible computational models that can represent all the functions in PRF. Firstly, we show that \(\textsf{For}_{\textsf{est}}\) extends Matos’ linear reversible computational model M-SRL, the very extension being a guaranteed terminating iteration that can be halted by means of logical predicates. The consequence is that \(\textsf{For}_{\textsf{est}}\) is PRF-complete, because M-SRL is. Secondly, we show that \(\textsf{For}_{\textsf{est}}\) is strictly algorithmically more expressive than M-SRL: it can encode a reversible algorithm for the minimum between two integers in optimal time, while M-SRL cannot.