Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible
summary
Presents a concrete equivalence: the Pi reversible language is shown equivalent to the free symmetric rig groupoid of finite sets and bijections via a denotational interpretation using denotational semantics via weak groupoids (Homotopy Type Theory style). Reductions from full Pi to a plus-only and then unary-indexed Pî yield a confluent, terminating rewrite system for adjacent transpositions, giving unique normal forms and a decidable equivalence procedure. Formalisation in a proof assistant generates normalization-by-evaluation and artifact code that synthesises and verifies reversible/quantum gates.
AI-written summary · about
chapters (4)
related talks
20mProto-Quipper with Reversing and Control
23mOne rig to control them all
27mPartial Evaluation of Reversible Flowchart Programs
32mA Finite Alternation Result for Reversible Boolean Circuits
24mA Computational Interpretation of Compact Closed Categories
17mMu tilde (re)cycled
18mIntroduction and Elimination, Left and Right
20mSemantic Reification: A New Paradigm for Random Program Generation