Finite Verification for Infinite Families of Diagram Equations

Hector Miller-Bakewell (University of Oxford)

The ZX, ZW and ZH calculi are all graphical calculi for reasoning about pure state qubit quantum mechanics. All of these languages use certain diagrammatic decorations, called !-boxes and phase variables, to indicate not just one diagram but an infinite family of diagrams. These decorations are powerful enough to allow complete rulesets for these calculi to be expressed in around ten rules. On the other hand reasoning involving decorated diagrams can be significantly more complicated. We present here a method for constructively reducing these infinite families of equations into finite verifying subsets. The only requirement for this construction is a property of our !-box structure that we call separability. This allows both researchers and proof assistants to reduce infinite families of problems down to undecorated, case-by-case verification, in a way not previously possible. In particular we note the removal of the need to reason directly with !-boxes in verification tasks as something entirely new, as well as extending a previously known result about removal of phase variables in verification tasks. This forms part of larger work in automated verification of quantum circuitry, and diagrammatic languages in general. The methods described here extend to any diagrammatic languages that meet certain simple conditions.