Finite Verification of Infinite Families of Diagram Equations

TL;DR

This paper introduces an algorithm that reduces infinite families of diagram equations with !-boxes in quantum graphical calculi to finite, verifiable subsets, enabling automated proof verification for complex quantum diagrams.

Contribution

It presents the first algorithm for finite verification of infinite diagram families involving !-boxes, applicable to ZX, ZW, and ZH calculi, with broad potential for other languages.

Findings

Algorithm successfully reduces infinite families to finite checks.

Extends previous finite phase variable analysis to !-boxes.

Enables proof assistants to verify complex quantum diagrams automatically.

Abstract

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 fifteen rules. Historically rules involving !-boxes have not been verifiable by computer. We present the first algorithm for reducing infinite families of equations involving !-boxes into finite verifying subsets. The only requirement for this method is a mild property on the connectivity of the !-boxes. Previous results had focussed on finite case analysis of phase variables in ZX, a result we also extend for ZW and ZH, as well as providing a general framework for further languages. The results presented here allow proof assistants to reduce infinite families of problems (involving combinations of phase variables and !-boxes) 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. This forms part of larger work in automated verification of quantum circuitry, conjecture synthesis, and diagrammatic languages in general. The methods described here extend to any diagrammatic languages that meet certain simple conditions.