Reconciling Partial and Local Invertibility

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.