Towards Term-based Verification of Diagrammatic Equivalence

TL;DR

This paper develops a formal framework for verifying the equivalence of diagrammatic representations, especially in quantum circuits, using normalizing term rewriting systems and proof assistants.

Contribution

It introduces normalizing term rewriting systems for diagrammatic equivalence and proves their termination and confluence using Isabelle/HOL.

Findings

Normalizing rewriting systems are effective for diagrammatic equivalence.

Termination and confluence are proven for the rewriting systems.

Framework supports automated reasoning in quantum circuit verification.

Abstract

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.