Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909061018025984 |
|---|---|
| author | Barile, Adriano Berardi, Stefano Roversi, Luca |
| author_facet | Barile, Adriano Berardi, Stefano Roversi, Luca |
| contents | Reversible Boolean Circuits are an interesting computational model under many aspects and in different fields, ranging from Reversible Computing to Quantum Computing. Our contribution is to describe a specific class of Reversible Boolean Circuits - which is as expressive as classical circuits - as a bi-dimensional diagrammatic programming language. We uniformly represent the Reversible Boolean Circuits we focus on as a free 3-category Toff. This formalism allows us to incorporate the representation of circuits and of rewriting rules on them, and to prove termination of rewriting. Termination follows from defining a non-identities-preserving functor from our free 3-category Toff into a suitable 3-category Move that traces the "moves" applied to wires inside circuits. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_02091 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem Barile, Adriano Berardi, Stefano Roversi, Luca Logic in Computer Science Category Theory Reversible Boolean Circuits are an interesting computational model under many aspects and in different fields, ranging from Reversible Computing to Quantum Computing. Our contribution is to describe a specific class of Reversible Boolean Circuits - which is as expressive as classical circuits - as a bi-dimensional diagrammatic programming language. We uniformly represent the Reversible Boolean Circuits we focus on as a free 3-category Toff. This formalism allows us to incorporate the representation of circuits and of rewriting rules on them, and to prove termination of rewriting. Termination follows from defining a non-identities-preserving functor from our free 3-category Toff into a suitable 3-category Move that traces the "moves" applied to wires inside circuits. |
| title | Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2401.02091 |