Leibniz international proceedings in informatics

Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi

Dichuan, Razin Abdulrauf Shaikh, Aleks Kissinger

Published Jan 1, 2026• 0 citations

Abstract

We introduce Graphical Algebraic Geometry (GAG), a family of diagrammatic languages extending the Graphical Linear Algebra programme. We construct several languages within this family and prove that they are universal and complete for the corresponding (co)span semantics of commutative algebras and affine varieties. This framework provides clear graphical representations of algebraic structures - such as polynomials, ideals, and varieties - enabling intuitive yet rigorous diagrammatic reasoning. We showcase two practical viewpoints on GAG. First, we show that instances of counting constraint satisfaction problem (#CSP) are recast as rewrite problems of closed diagrams in GAG. This means that deciding rewritability in GAG is #P-hard, and GAG can be viewed as a complete and compositional rewrite system for networks of polynomial constraints. Second, we characterize the qudit ZH calculus, a diagrammatic language for quantum computation, as an extension of Graphical Algebraic Geometry. This establishes the correspondence that Graphical Algebraic Geometry is to the ZH calculus what Graphical Linear Algebra is to the ZX calculus. Using this construction, we show that computing amplitudes in qudit ZH requires only a constant number of queries to a GAG oracle.

DOI: 10.4230/lipics.lics.2026.48

Related papers

Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi

Dichuan Gao, Razin A. Shaikh, Aleks Kissinger

We introduce Graphical Algebraic Geometry (GAG), a family of diagrammatic languages extending the Graphical Linear Algebra programme. We construct several languages within this family and prove that they are universal and complete for the corresponding (co)span semantics of commutative algebras and affine varieties. This framework provides clear graphical representations of algebraic structures -- such as polynomials, ideals, and varieties -- enabling intuitive yet rigorous diagrammatic reasoning. We showcase two practical viewpoints on GAG. First, we show that instances of counting constraint satisfaction problem (#CSP) are recast as rewrite problems of closed diagrams in GAG. This means that deciding rewritability in GAG is #P-hard, and GAG can be viewed as a complete and compositional rewrite system for networks of polynomial constraints. Second, we characterize the qudit ZH calculus, a diagrammatic language for quantum computation, as an extension of Graphical Algebraic Geometry. This establishes the correspondence that Graphical Algebraic Geometry is to the ZH calculus what Graphical Linear Algebra is to the ZX calculus. Using this construction, we show that computing amplitudes in qudit ZH requires only a constant number of queries to a GAG oracle.

quant-pharXiv:2605.13993May 15, 20260 citations

Graphical Symplectic Algebra

Robert I. Booth, Titouan Carette, Cole Comfort

We introduce a family of diagrammatical equational theories unifying two research programs: categorical quantum mechanics and graphical linear algebra. We prove their completeness with respect to denotational semantics described in terms of relations between vector spaces equipped with symplectic structure. This provides versatile graphical languages encompassing both affinely constrained classical mechanical systems, as well as odd-prime-dimensional stabiliser and Gaussian quantum circuits. Terms are described by labelled graphs with input and output interfaces, and the languages are equipped with equational theories amenable to standard graph rewriting techniques. In order to reason about large composite systems, we introduce a compact scalable notation where the vertices are themselves labelled by graphs. This notation allows us to state new and powerful rewrite rules which operate on diagrams at a large scale. We also show how this notation neatly captures some important constructions, such as graph states of quantum computing and the impedance and admittance matrices of electrical networks.

arXiv:2401.07914Leibniz international proceedings in informaticsJan 15, 20241 citation

Graphical Calculi and their Conjecture Synthesis

Hector Miller-Bakewell

Categorical Quantum Mechanics, and graphical calculi in particular, has proven to be an intuitive and powerful way to reason about quantum computing. This work continues the exploration of graphical calculi, inside and outside of the quantum computing setting, by investigating the algebraic structures with which we label diagrams. The initial aim for this was Conjecture Synthesis; the algorithmic process of creating theorems. To this process we introduce a generalisation step, which itself requires the ability to infer and then verify parameterised families of theorems. This thesis introduces such inference and verification frameworks, in doing so forging novel links between graphical calculi and fields such as Algebraic Geometry and Galois Theory. These frameworks inspired further research into the design of graphical calculi, and we introduce two important new calculi here. First is the calculus RING, which is initial among ring-based qubit graphical calculi, and in turn inspired the introduction and classification of phase homomorphism pairs also presented here. The second is the calculus ZQ, an edge-decorated calculus which naturally expresses arbitrary qubit rotations, eliminating the need for non-linear rules such as (EU) of ZX. It is expected that these results will be of use to those creating optimisation schemes and intermediate representations for quantum computing, to those creating new graphical calculi, and for those performing conjecture synthesis.

arXiv:2010.03914Jan 1, 20201 citation

An Algebraic Axiomatisation of ZX-calculus

Quanlong Wang

ZX-calculus is a graphical language for quantum computing which is complete in the sense that calculation in matrices can be done in a purely diagrammatic way. However, all previous universally complete axiomatisations of ZX-calculus have included at least one rule involving trigonometric functions such as sin and cos which makes it difficult for application purpose. In this paper we give an algebraic complete axiomatisation of ZX-calculus instead such that there are only ring operations involved for phases. With this algebraic axiomatisation of ZX-calculus, we are able to establish for the first time a simple translation of diagrams from another graphical language called ZH-calculus and to derive all the ZX-translated rules of ZH-calculus. As a consequence, we have a great benefit that all techniques obtained in ZH-calculus can be transplanted to ZX-calculus, which can't be obtained by just using the completeness of ZX-calculus.

arXiv:1911.06752Electronic Proceedings in Theoretical Computer ScienceSep 6, 202114 citations

Vy ZX: Formal Verification of a Graphical Quantum Language

Adrian Lehmann, Ben Caldwell, Bhakti Shah +2 more

Graphical languages are a convenient shorthand to represent computation, with rewrite rules relating one graph to another. In contrast, proof assistants rely heavily on inductive datatypes, particularly when giving semantics to embedded languages. This creates obstacles to formally reasoning about graphical languages, since imposing an inductive structure obfuscates the diagrammatic nature of graphical languages, along with their corresponding equational theories. To address this gap, we present Vy ZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category-theoretic definitions. We developed Vy ZX to V erify the ZX -calculus, a graphical language for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph’s semantic interpretation. We show how inductive graphs in Vy ZX are used to prove the soundness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. We also provide an IDE-integrated visualizer for proof engineers to directly reason about diagrams in graphical form.

ACM Transactions on Programming Languages and SystemsApr 11, 20263 citations

VyZX: Formal Verification of a Graphical Quantum Language

Adrian Lehmann, Ben Caldwell, Bhakti Shah +2 more

Graphical languages are a convenient shorthand to represent computation, with rewrite rules relating one graph to another. In contrast, proof assistants rely heavily on inductive datatypes, particularly when giving semantics to embedded languages. This creates obstacles to formally reasoning about graphical languages, since imposing an inductive structure obfuscates the diagrammatic nature of graphical languages, along with their corresponding equational theories. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category-theoretic definitions. We developed VyZX to Verify the ZX-calculus, a graphical langauge for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph's semantic interpretation. We show how inductive graphs in VyZX are used to prove the soundness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. We also provide an IDE-integrated visualizer for proof engineers to directly reason about diagrams in graphical form.

arXiv:2311.11571Nov 20, 20231 citation