This repository contains the accompanying formalisation for the POPL'22 paper "Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages".
- Main Repository: https://github.com/vikraman/popl22-symmetries-artifact
- Source Code: https://vikraman.github.io/popl22-symmetries-artifact
- Zenodo: https://zenodo.org/record/5554623
The purpose of this artifact is to:
-
Provide a partial formalisation of the semantics presented in the paper and related results.
-
Show applications of the semantics, using a collection of examples showing normalisation-by-evaluation, synthesis, and equivalence of reversible circuits written in the Pi language.
The formalisation has been checked using Agda 2.6.1.3 and the HoTT-Agda library (using Andrew Swan's fork).
The easiest way to install Agda on your machine is using stack.
-
Install stack following the instructions on the official website: https://docs.haskellstack.org/
-
Install Agda using stack (tested using ghc 8.10.4 and resolver 17.15).
$ stack install Agda-2.6.1.3Then, clone this repository (including submodules recursively) and use the provided Makefile. The repository uses a submodule which contains the main formalisation and library submodules (and more related work on Pi).
$ git clone --recursive https://github.com/vikraman/popl22-symmetries-artifact
$ cd popl22-symmetries-artifactTo count the number of lines, we use cloc which can be installed using a package manager.
We also provide a prebuilt docker image (linux/amd64) with all tools and libraries installed.
$ docker pull vikraman/popl22-symmetries-artifact
$ docker run -it --rm vikraman/popl22-symmetries-artifact bashWe provide a Makefile whose default target checks the Pi/Everything.agda file.
$ makeOr, it can also exhaustively check every file in the Pi directory.
$ make reallyallAlternatively, you can check individual files in agda, and step through each term interactively.
To step through the proofs and examples interactively, one has to use the interactive Agda mode, which is available for Emacs and VSCode. To use it:
-
In Emacs, simply use
agda-mode locateand load the file to get the major mode for Agda. UseC-c C-lto load the Agda file, andC-u C-c C-nto compute the normal form of a term. -
In VSCode, install
agda-modeextension and point it to the location of Agda executable in your system. The usage instructions are provided in the extension's documentation. To load the file, useC-c C-l. After loading the file, inspect the normal form of a chosen expression by usingC-u C-n.
To count the number of lines, run:
$ make cloc
To list the TODOs in the formalisation, run:
$ make todos
As a convention, the ones marked TODO! are the important ones, and the ones marked TODO- are trivial.
This repository contains the formalisation of the denotational semantics of Pi, accompanying the paper.
Pi/Everything.agda is the main entrypoint to the project. The Agda source is also hosted as interactive html
here.
Each subdirectory has its own README file, which describes the files in that directory, and is a good starting point to understanding the high-level structure of the code.
Pi.Common: Common lemmas and definitions about natural numbers and lists, used in the project.Pi.Coxeter: Definition and properties of the Coxeter relation and the rewriting system based on it.Pi.Equiv: The main proof of equivalence between Pi and UFin.Pi.Examples: Examples of reversible boolean circuits showing applications of the semantics.Pi.Experiments: Various experiments, alternative approaches and earlier results.Pi.FSMG: Free symmetric monoidal groupoids.Pi.Lehmer: Lehmer codes.Pi.Syntax: Syntax of Pi and its variants.Pi.UFin: Construction of UFin and various properties.
This section presents the syntax of Pi and its soundness with respect to finite sets and bijections.
| Claim | Formalisation |
|---|---|
| Figure 3 | Pi/Syntax/Pi.agda |
| Theorem 3.1.1 | Pi/Examples/Interp.agda |
This section develops the theory of univalent subuniverses, and the construction of
| Claim | Formalisation |
|---|---|
| Definition 4.1 | Pi/UFin/Univ.agda#L25 |
| Definition 4.2 | Pi/UFin/Univ.agda#L42 |
| Proposition 4.3 | Pi/UFin/Univ.agda#L76 |
| Definition 4.4 | HoTT-Agda/core/lib/types/Fin.agda |
| Definition 4.5 | HoTT-Agda/theorems/homotopy/FinSet.agda#L13 |
| Lemma 4.6 | HoTT-Agda/theorems/homotopy/FinSet.agda#L51 |
| Definition 4.7 | HoTT-Agda/theorems/homotopy/FinSet.agda#L10 |
| Definition 4.8 | HoTT-Agda/core/lib/types/BAut.agda#L10 |
| Definition 4.9 | Pi/UFin/Base.agda |
| Lemma 4.10.1 | Pi/UFin/BAut.agda#L31 |
| Lemma 4.10.2 | HoTT-Agda/core/lib/types/BAut.agda#L27 |
| Lemma 4.10.3 | Pi/UFin/BAut.agda#63 |
| Theorem 4.11 | Pi/UFin/Base.agda#L18 |
| Proposition 4.12 | Pi/UFin/Monoidal.agda |
| Theorem 4.13 | Pi/UFin/Monoidal.agda |
The main theorems in the section - equivalences between Sn, normalisation function image and Lehmer codes - appear
exactly in the Agda code. The intermediate steps were, however, slightly modified in the paper, to simplify the
presentation. The main difference is that the main proofs of the properties of Coxeter relations are initially done, for
technical and historical reasons, without using parametrising it over n - i.e., working on List ℕ instead of List (Fin n), (Pi/Coxeter/NonParametrized),
and only later is this changed, in
(Pi/Coxeter/Parametrized).
Another difference is that, again for mostly historical reasons, we have used two definitions of Lehmer codes (Pi/Lehmer/Lehmer.agda and Pi/Lehmer/Lehmer2.agda), and proved them to be equivalent.
The functions marked with {-# TERMINATING #-} can be proved terminating on paper, using the fact that the Coxeter
reduction relation decreases the lexicographical order of words.
This section presents the equivalence between the syntax and semantics. In the formalisation, this is done by
constructing functions eval/quote for 0, 1, and 2-cells, between each variant of the language and finally with UFin.
Instead of following the list of claims in the text, we state what each file does.
- Pi/Syntax/Pi+/NonIndexed.agda: (Non-indexed) syntax for Pi+.
- Pi/Syntax/Pi+/Indexed.agda: (Indexed) syntax for Pi+.
- Pi/Syntax/Pi^.agda: Syntax for Pi^.
- Pi/Equiv/Equiv0.agda: The proof of equivalence between Pi+ types and 0-cells in UFin. A composition of:
- Pi/Equiv/Equiv0Hat.agda: The proof of equivalence between Pi+ types and Pi^ types.
- Pi/Equiv/Equiv0Norm.agda: The proof of equivalence between Pi^ types (natural numbers) and 0-cells in UFin.
- Pi/Equiv/Equiv1.agda: The proof of equivalence between the 1-combinators of Pi+ and 1-paths in UFin. A composition of:
- Pi/Equiv/Equiv1Hat.agda: The proof of equivalence between Pi+ 1-combinators and Pi^ 1-combinators.
- Pi/Equiv/Equiv1Norm.agda: The proof of equivalence between Pi^ 1-combinators and 1-cells in UFin.
- Pi/Equiv/Equiv2.agda: The proof of equivalence between the 2-combinators of Pi+ and 2-paths in UFin. A composition of:
- Pi/Equiv/Equiv2Hat.agda: The proof of equivalence between Pi+ 1-combinators and Pi^ 1-combinators.
- Pi/Equiv/Equiv2Norm.agda: The proof of equivalence between Pi^ 2-combinators and 2-paths in UFin.
- Pi/Equiv/Translation2.agda: Translation of Pi to Pi+ and back.
- Pi/Examples/Interp.agda - The interpreters for Pi, Pi+, Pi^.
The formalisation includes several examples, including those mentioned in the paper, and others. Despite postulates, the examples are written in such a way that they will compute (with some caveats).
The files are more-or-less self-documented -- we define each reversible circuit, compute their normal forms, then quote
them back, step-by-step using the semantics. One can inspect each term using Agda's interactive mode, using the "Compute
Normal Form" command (in Emacs, make sure to add C-u to compute the most normalised form).
Note that computing normal forms for some circuits can be really slow.
- Pi/Examples/Adder.agda: Reversible 3-bit/4-bit adder.
- Pi/Examples/Base.agda: Helpers and tests.
- Pi/Examples/Copy.agda: Reversible copy.
- Pi/Examples/ExamplesL.lagda: Examples used in the paper text,
reversibleOrNormfunction is implemented asadder3in Pi/Examples/Adder.agda. - Pi/Examples/ExpMod.agda: Reversible exponentiation modulo 2^n.
- Pi/Examples/Incr.agda: Reversible increment.
- Pi/Examples/Interp.agda: Interpreters for 1-combinators of Pi, Pi+, Pi^, and various tests.
- Pi/Examples/Reset.agda: Reversible reset.
- Pi/Examples/Toffoli.agda: Toffoli gate (controlled controlled NOT)
- In the formalisation, there is an additional step of going through Pi+ variant where types are indexed by their
cardinality, this makes it easier to write some proofs which perform induction on the syntax, and eliminate some
absurd cases (using the
eq-sizerewrite). - Proving termination for certain functions is difficult in Agda, and we assert they're terminating. On paper, it is easy to see that they terminate.
- In HoTT-Agda, univalence/HITs are asserted as postulates, and they don't compute. Further, computing or proving with the identity type relies on beta/eta reduction done "by hand", which is not explicitly done in the paper. This makes some formalised proofs verbose.
- Using the formalised rewriting system to compute the normalisation function is very slow. We include several examples in the formalisation and it takes a while to compute them. Some computations are intractable, and we have left them commented out.
- Translating commutative diagrams for large coherence results to Pi syntax using combinators is tedious. Similarly,
using decidable equality and case matches to define large functions and reductions and then proving things about
them is tedious. Some parts of the formalisation have been left as
TODOs but we provide references for them, or give a proof outline on paper. FSMGis a HIT for free symmetric monoidal groupoids, this is experimental and left as future work.Experimentscontains alternative definitions using HITs and some earlier attempts at proving the main equivalence.