一句话：为可逆布尔电路语言 Pi 建立基于弱 groupoid 的指称语义，并证明其与有限类型 univalent 子宇宙的 groupoid 等价及 Curry–Howard–Lambek 对应。
可逆编程语言 Pi 族以见证代数数据类型类型同构的组合子语法呈现，但此前缺乏指称语义与等式理论。本文用 Homotopy Type Theory 风格的弱 groupoid 给出指称语义，并以 2-combinator 导出等式理论。作者建立语言语法 groupoid 与有限类型 univalent 子宇宙的对应：1-combinator 对应 1-path，2-combinator 对应 2-path，并证明两个层次均可靠完备，形成 groupoid 等价。由此得到可逆逻辑、可逆编程语言与对称 rig groupoid 间的 Curry–Howard–Lambek 对应，说明 Pi 语法由有限集合与双射给出的自由对称 rig groupoid 呈现。基于形式化，作者实现 normalization-by-evaluation，并用于可逆逻辑门的验证与综合，示例受量子计算启发，还展示不同电路表示间定理的推理与迁移。
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.
@article{paperbot1594,
title = {Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages},
author = {Vikraman Choudhury and Jacek Karwowski and Amr Sabry},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498667}
}