kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Reconciling Partial and Local Invertibility
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Software and Computer systems, SCS. Tohoku University, Aramaki Aza-aoba 6-3-09, Aoba-ku, 980-8579, Sendai, Japan, Aramaki Aza-aoba 6-3-09, Aoba-ku.ORCID iD: 0009-0008-0847-5373
Tohoku University, Aramaki Aza-aoba 6-3-09, Aoba-ku, 980-8579, Sendai, Japan, Aramaki Aza-aoba 6-3-09, Aoba-ku.
University of Bristol, BS8 1TH, Bristol, UK.
2024 (English)In: Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Springer Nature , 2024, Vol. 14577, p. 59-89Conference paper, Published paper (Refereed)
Abstract [en]

Invertible programming languages specify transformations to be run in two directions, such as compression/decompression or encryption/decryption. Two key concepts in invertible programming languages are partial invertibility and local invertibility. Partial invertibility lets invertible code be parameterized by the results of non-invertible code, whereas local invertibility requires all code to be invertible. The former allows for more flexible programming, while the latter has connections to domains such as low-energy computing and quantum computing. We find that existing approaches lack a satisfying treatment of partial invertibility, leaving the connection to local invertibility unclear. In this paper, we identify four core constructs for partially invertible programming, and show how to give them a locally invertible interpretation. We show the expressiveness of the constructs by designing the functional invertible language Kalpis, and show how to give them a locally invertible semantics using the novel arrow combinator language RRARR—the key idea is viewing partial invertibility as an invertible effect. By formalizing the two systems and giving Kalpis semantics by translation to RRARR, we reconcile partial and local invertibility, solving an open problem in the field. All formal developments are mechanized in Agda.

Place, publisher, year, edition, pages
Springer Nature , 2024. Vol. 14577, p. 59-89
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 14577
Keywords [en]
Arrows, Domain-specific languages, Partial invertibility, Reversible computation
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-346542DOI: 10.1007/978-3-031-57267-8_3ISI: 001281762600003Scopus ID: 2-s2.0-85192157494OAI: oai:DiVA.org:kth-346542DiVA, id: diva2:1858458
Conference
33rd European Symposium on Programming, ESOP 2024, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, Apr 6 2024 - Apr 11 2024
Note

QC 20240521

Part of ISBN 978-303157266-1

Available from: 2024-05-16 Created: 2024-05-16 Last updated: 2024-09-12Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Ågren Thuné, Anders

Search in DiVA

By author/editor
Ågren Thuné, Anders
By organisation
Software and Computer systems, SCS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 52 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf