English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The $\mathit{\Pi}$ family of reversible programming languages for booleancircuits is presented as a syntax of combinators witnessing type isomorphismsof algebraic datatypes. In this paper, we give a denotational semantics forthis language, using the language of weak groupoids \`a la Homotopy TypeTheory, and show how to derive an equational theory for it, presented by2-combinators witnessing equivalences of reversible circuits. We establish acorrespondence between the syntactic groupoid of the language and a formallypresented univalent subuniverse of finite types. The correspondence relates1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, whichis shown to be sound and complete for both levels, establishing fullabstraction and adequacy. We extend the already established Curry-Howardcorrespondence for $\mathit{\Pi}$ to a Curry-Howard-Lambek correspondencebetween Reversible Logic, Reversible Programming Languages, and Symmetric RigGroupoids, by showing that the syntax of $\mathit{\Pi}$ is presented by thefree symmetric rig groupoid, given by finite sets and permutations. Our proofuses techniques from the theory of group presentations and rewriting systems tosolve the word problem for symmetric groups. Using the formalisation of ourresults, we show how to perform normalisation-by-evaluation, verification, andsynthesis of reversible logic gates, motivated by examples from quantumcomputing.

Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages