Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

matos2020tcs (Article)
Author(s) Armando B. Matos, Luca Paolini and Luca Roversi
Title« The fixed point problem of a simple reversible language »
JournalTheoretical Computer Science
Volume813
Page(s)143 - 154
Year2020
ISSN number0304-3975
URLhttp://www.sciencedirect.com/science/article/pii/S0304397519306280
Abstract & Keywords
SRL is a total programming language with distinctive features: (i) every program that mentions n registers defines a bijection Zn→Zn, and (ii) the generation of the SRL-program that computes the inverse of that bijection can be automatic. Containing SRL a very essential set of commands, it is suitable for studying strengths and weaknesses of reversible computations. We deal with the fixed points of SRL-programs. Given any SRL-program P, we are interested in the problem of deciding if a tuple of initial register values of P exists which remains unaltered after its execution. We show that the existence of fixed points in SRL is undecidable and complete in Σ10. We show that such problem remains undecidable even when the number of registers mentioned by P is limited to 12. Moreover, if we restrict to the linear programs of SRL, i.e. to those programs where different registers control nested loops, then the problem is already undecidable for the class of SRL-programs that mention no more than 3712 registers. Last, we show that, except for trivial cases, finding if the number of fixed points has a given cardinality is also undecidable.

Keywords: Reversible computing, Fixed points, Decidability

BibTeX code

@article{matos2020tcs,
  volume = {813},
  author = {Armando B. Matos and Luca Paolini and Luca Roversi},
  issn = {0304-3975},
  keywords = {Reversible computing, Fixed points, Decidability},
  url = {http://www.sciencedirect.com/science/article/pii/S0304397519306280},
  abstract = {SRL is a total programming language with distinctive features: (i)
              every program that mentions n registers defines a bijection
              Zn→Zn, and (ii) the generation of the SRL-program that computes
              the inverse of that bijection can be automatic. Containing SRL a
              very essential set of commands, it is suitable for studying
              strengths and weaknesses of reversible computations. We deal with
              the fixed points of SRL-programs. Given any SRL-program P, we are
              interested in the problem of deciding if a tuple of initial
              register values of P exists which remains unaltered after its
              execution. We show that the existence of fixed points in SRL is
              undecidable and complete in Σ10. We show that such problem
              remains undecidable even when the number of registers mentioned by
              P is limited to 12. Moreover, if we restrict to the linear
              programs of SRL, i.e. to those programs where different registers
              control nested loops, then the problem is already undecidable for
              the class of SRL-programs that mention no more than 3712
              registers. Last, we show that, except for trivial cases, finding
              if the number of fixed points has a given cardinality is also
              undecidable.},
  title = {The fixed point problem of a simple reversible language},
  pages = {143 - 154},
  journal = {Theoretical Computer Science},
  doi = {https://doi.org/10.1016/j.tcs.2019.10.005},
  year = {2020},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!