Towards Term-based Verification of Diagrammatic Equivalence
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910019369304064 |
|---|---|
| author | Cailler, Julie Delorme, Noé Perdrix, Simon Tourret, Sophie |
| author_facet | Cailler, Julie Delorme, Noé Perdrix, Simon Tourret, Sophie |
| contents | A string diagram is a two-dimensional graphical representation that can be described as a one-dimensional term generated from a set of primitives using sequential and parallel compositions. Since different syntactic terms may represent the same diagram, this syntax is quotiented by a collection of coherence equations expressing equivalence up to deformation. This work lays foundations for automated reasoning about diagrammatic equivalence, motivated primarily by the verification of quantum circuit equivalences. We consider two classes of diagrams, for which we introduce normalizing term rewriting systems that equate diagrammatically equivalent terms. In both cases, we prove termination and confluence with the help of the proof assistant Isabelle/HOL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_11035 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Towards Term-based Verification of Diagrammatic Equivalence Cailler, Julie Delorme, Noé Perdrix, Simon Tourret, Sophie Logic in Computer Science A string diagram is a two-dimensional graphical representation that can be described as a one-dimensional term generated from a set of primitives using sequential and parallel compositions. Since different syntactic terms may represent the same diagram, this syntax is quotiented by a collection of coherence equations expressing equivalence up to deformation. This work lays foundations for automated reasoning about diagrammatic equivalence, motivated primarily by the verification of quantum circuit equivalences. We consider two classes of diagrams, for which we introduce normalizing term rewriting systems that equate diagrammatically equivalent terms. In both cases, we prove termination and confluence with the help of the proof assistant Isabelle/HOL. |
| title | Towards Term-based Verification of Diagrammatic Equivalence |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.11035 |