Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi

TL;DR

The paper presents a workflow that uses LMNtal and its quantified extension QLMNtal to encode ZX-calculus diagrams and rewrite rules declaratively, enabling formal verification of optimization strategies through state-space exploration and model checking. It demonstrates that QLMNtal can express arbitrary-arity ZX rules with a single rule, and uses state-space and LTL analyses to study the behavior of rewriting strategies and inductive proofs. Through case studies on quantum teleportation and GHZ preparation, the approach shows how non-confluent rules and strategy design influence optimization paths and final diagram simplicity, while also providing tooling (converter, visualizers) to support practical experimentation. The work positions LMNtal/QLMNtal as an open platform for strategic experimentation in quantum circuit transformation and proposes extensions to other calculi and standard formats to broaden applicability.

Abstract

Systematic discovery of optimization paths in quantum circuit simplification remains a challenge. Today, ZX-calculus, a computing model for quantum circuit transformation, is attracting attention for its highly abstract graph-based approach. Whereas existing tools such as PyZX and Quantomatic offer domain-specific support for quantum circuit optimization, visualization and theorem-proving, we present a complementary approach using LMNtal, a general-purpose hierarchical graph rewriting language, to establish a diagrammatic transformation and verification platform with model checking. Our methodology shows three advantages: (1) manipulation of ZX-diagrams through native graph transformation rules, enabling direct implementation of basic rules; (2) quantified pattern matching via QLMNtal extensions, greatly simplifying rule specification; and (3) interactive visualization and validation of optimization paths through state space exploration. Through case studies, we demonstrate how our framework helps understand optimization paths and design new algorithms and strategies. This suggests that the declarative language LMNtal and its toolchain could serve as a new platform to investigate quantum circuit transformation from a different perspective.

Figures (23)

• Figure 1: Syntax of LMNtal.
• Figure 2: Rewriting with (o(L),{x(L),$p}) :- {y,$p} .
• Figure 3: Rewriting with Rules zxh (upper) and zxb (lower).
• Figure 4: Key Rewrite Rules in ZX-Calculus vandewetering_zx-calculus_2020. (f): spider fusion, (h): color change (b): (generalized) bialgebra rule, ($\pi$): $\pi$ commutation, (c): copy, (id): identity, (hh): Hadamard cancellation, (hopf): Hopf.
• Figure 5: ZX-rules based on local complementation and pivoting. Blue dotted wires are wires with a Hadamard gate vandewetering_zx-calculus_2020.