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.

The fixed point problem of a simple reversible language

Armando Matos;Luca Paolini;Luca Roversi
2020-01-01

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.
813
143
154
http://www.sciencedirect.com/science/article/pii/S0304397519306280
Reversible computing, Fixed points, Decidability
Armando Matos, Luca Paolini, Luca Roversi
File in questo prodotto:
File Dimensione Formato  
20-03-23-main-caricato-su-IRIS.pdf

Accesso aperto

Descrizione: Author's post-print con data di accettazione 06 10 2019
Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 334.98 kB
Formato Adobe PDF
334.98 kB Adobe PDF Visualizza/Apri
The fixed point problem of a simple reversible language - TCS 2019 ori.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 404.46 kB
Formato Adobe PDF
404.46 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1734164
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact