Symmetries in reversible programming

from symmetric rig groupoids to reversible programming languages

conference
groupoids
groups
homotopy type theory
permutations
reversible computing
reversible programming languages
rewriting
type isomorphisms
univalent foundations
Authors
Affiliations

Vikraman Choudhury

Indiana University, USA / University of Cambridge, UK

Jacek Karwowski

University of Warsaw, Poland

Amr Sabry

Indiana University, USA

Published

January 12, 2022

Doi

10.1145/3498667

Abstract

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms.

We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections.

Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.

Keywords

groupoids, groups, homotopy type theory, permutations, reversible computing, reversible programming languages, rewriting, type isomorphisms, univalent foundations

Back to top

Citation

BibTeX citation:
@inproceedings{choudhury2022,
  author = {Choudhury, Vikraman and Karwowski, Jacek and Sabry, Amr},
  title = {Symmetries in Reversible Programming},
  booktitle = {Proceedings of the ACM on Programming Languages},
  date = {2022},
  url = {https://doi.org/10.1145/3498667},
  doi = {10.1145/3498667},
  langid = {en},
  abstract = {The Pi family of reversible programming languages for
    boolean circuits is presented as a syntax of combinators witnessing
    type isomorphisms of algebraic data types. In this paper, we give a
    denotational semantics for this language, using weak groupoids à la
    Homotopy Type Theory, and show how to derive an equational theory
    for it, presented by 2-combinators witnessing equivalences of type
    isomorphisms. We establish a correspondence between the syntactic
    groupoid of the language and a formally presented univalent
    subuniverse of finite types. The correspondence relates
    1-combinators to 1-paths, and 2-combinators to 2-paths in the
    universe, which is shown to be sound and complete for both levels,
    forming an equivalence of groupoids. We use this to establish a
    Curry-Howard-Lambek correspondence between Reversible Logic,
    Reversible Programming Languages, and Symmetric Rig Groupoids, by
    showing that the syntax of Pi is presented by the free symmetric rig
    groupoid, given by finite sets and bijections. Using the
    formalisation of our results, we perform
    normalisation-by-evaluation, verification and synthesis of
    reversible logic gates, motivated by examples from quantum
    computing. We also show how to reason about and transfer theorems
    between different representations of reversible circuits.}
}
For attribution, please cite this work as:
Choudhury, Vikraman, Jacek Karwowski, and Amr Sabry. 2022. “Symmetries in Reversible Programming.” Proceedings of the ACM on Programming Languages, accepted. https://doi.org/10.1145/3498667.