Reconciling Partial and Local Invertibility
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
2024-05-162024-05-162024-09-12Bibliographically approved