Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Flow Diagrams, Assertions, and Formal Methods Kapitel lesen Erstes Kapitel lesen

2020 | OriginalPaper | Buchkapitel

Reversible Programs Have Reversible Semantics

verfasst von : Robert Glück, Robin Kaarsgaard, Tetsuo Yokoyama

Erschienen in: Formal Methods. FM 2019 International Workshops

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

During the past decade, reversible programming languages have been formalized using various established semantic frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, and even neglect the central question of whether the defined language is reversible. In this paper, we build on a metalanguage foundation for reversible languages based on the category of sets and partial injective functions. We exemplify our approach through step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. This yields a formalization of the semantics in which the reversibility of the language and its inverse semantics are immediate, as well as the inversion of programs written in the language. We further discuss applications and future research directions for reversible semantics.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Comparing Correctness-by-Construction with Post-Hoc Verification—A Qualitative User Study
Nächstes Kapitel Two-Way Quantum and Classical Automata with Advice for Online Minimization Problems
Fußnoten
1
An online interpreter for R-WHILE with procedures and the example program considered in this paper are available at http://​tetsuo.​jp/​ref/​RPLA2019.
 
Literatur
1.
2.
Cockett, R., Lack, S.: Restriction categories III: colimits, partial limits and extensivity. Math. Struct. Comput. Sci. 17(4), 775–817 (2007)MathSciNetCrossRef
3.
Frank, M.P.: Reversibility for efficient computing. Ph.D. thesis, MIT (1999)
4.
Giles, B.: An investigation of some theoretical aspects of reversible computing. Ph.D. thesis, University of Calgary (2014)
5.
Glück, R., Kaarsgaard, R.: A categorical foundation for structured reversible flowchart languages: Soundness and adequacy. Log. Methods Comput. Sci. 14(3) (2018)
6.
Glück, R., Kawabe, M.: Revisiting an automatic program inverter for Lisp. SIGPLAN Not. 40(5), 8–17 (2005)CrossRef
7.
Glück, R., Yokoyama, T.: A minimalist’s reversible while language. IEICE Trans. Inf. Syst. E100-D 100(5), 1026–1034 (2017)CrossRef
8.
Glück, R., Yokoyama, T.: Constructing a binary tree from its traversals by reversible recursion and iteration. IPL 147, 32–37 (2019)MathSciNetCrossRef
9.
Haghverdi, E.: A categorical approach to linear logic, geometry of proofs and full completeness. Ph.D. thesis, Carlton Univ. and Univ. Ottawa (2000)
10.
Hoey, J., Ulidowski, I., Yuen, S.: Reversing parallel programs with blocks and procedures. In: Pérez, J.A., Tini, S. (eds.) Expressiveness in Concurrency, Structural Operational Semantics. Electronic Proceedings in TCS, vol. 276, pp. 69–86 (2018)
11.
12.
James, R.P., Sabry, A.: Information effects. In: POPL, pp. 73–84. ACM (2012)
13.
Kaarsgaard, R., Axelsen, H.B., Glück, R.: Join inverse categories and reversible recursion. J. Log. Algebr. Methods 87, 33–50 (2017)MathSciNetMATH
14.
Kari, J.: Reversible cellular automata: from fundamental classical results to recent developments. New Gener. Comput. 36(3), 145–172 (2018)CrossRef
15.
16.
Morita, K.: Reversible computing and cellular automata – a survey. Theor. Comput. Sci. 395(1), 101–131 (2008)MathSciNetCrossRef
17.
18.
Wille, R., Schönborn, E., Soeken, M., Drechsler, R.: SyReC: a hardware description language for the specification and synthesis of reversible circuits. Integration 53, 39–53 (2016)CrossRef
19.
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)CrossRef
20.
21.
Yokoyama, T., Axelsen, H.B., Glück, R.: Fundamentals of reversible flowchart languages. Theor. Comput. Sci. 611, 87–115 (2016)MathSciNetCrossRef
22.
Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: PEPM, pp. 144–153. ACM (2007)
Metadaten
Titel
Reversible Programs Have Reversible Semantics
verfasst von
Robert Glück
Robin Kaarsgaard
Tetsuo Yokoyama
Copyright-Jahr
2020
Buch
Formal Methods. FM 2019 International Workshops

Print ISBN: 978-3-030-54996-1

Electronic ISBN: 978-3-030-54997-8

Copyright-Jahr: 2020

DOI
https://doi.org/10.1007/978-3-030-54997-8_26