An Algebraic Axiomatisation of ZX-calculus

1 Introduction

• Prior universally complete ZX axiomatisations included rules with trigonometric functions such as sin and cos, which the paper identifies as difficult to use directly in applications.The introduction notes that such rules can turn simple angles into complicated ones.Source: §1 · pp. 1–2
• The paper gives a complete ZX axiomatisation using only ring operations for phases, with a new generator whose parameters range over complex numbers.The authors say the new rules can derive the rules of an earlier complete axiomatisation.Source: §1 · p. 2
• The algebraic rules support a simple translation of full ZH-calculus diagrams into ZX-calculus and derivations of all the translated ZH rules.The authors say this detailed derivation enables techniques from ZH-calculus to be transplanted to ZX-calculus.Source: §1 · p. 2

2 Algebraic axiomatisation of ZX-calculus

• Some generators, including T and T−1, can be expressed using the original green and red spiders, though the expression is complicated.The paper introduces these generators as part of its generator presentation.Source: §2 · pp. 2–3
• The proposed ZX rules involve no trigonometric functions, and the listed generators include parameters ranging over complex numbers.The authors describe the rule set as algebraic and say it is not unique; useful rules for applications are a key selection criterion.Source: Table 1 · p. 3, §2 · pp. 4, 6
• The authors say the algebraic rules are sound under the standard interpretation and can derive spider nest identities, which are key to quantum-circuit T-count reduction.The rules were refined through diagrammatic rewriting practice and an algebraic translation from ZW-calculus.Source: §2 · pp. 5–6

3 Proof of completeness

• Compared with the earlier axiomatisation, this system uses a green box parameterised by complex numbers rather than a yellow box parameterised by nonnegative real numbers.The paper also describes its triangle-involved rules as simpler and more natural than those in Figure 3.Source: §3 · p. 9
• The algebraic rules in Figure 1 make ZX-calculus complete for pure qubit quantum mechanics.The proof strategy is to derive the rules in Figures 2 and 3, already known to be complete, from Figure 1.Source: §3 · pp. 6, 9

4 From ZH-calculus to ZX-calculus

• The paper gives a semantics-preserving translation from any ZH diagram to a ZX diagram and derives all the translated ZH rules within ZX-calculus.The authors identify the derivations, especially for the last three ZH rules, as nontrivial.Source: §4 · p. 9
• The authors say the translation and rule derivations allow results obtained via ZH-calculus to be transplanted to ZX-calculus.Source: §4 · p. 9
• The white spider in ZH-calculus translates to the phase-free green spider in ZX-calculus.The translation of the H-box is used to define the translation from ZH to ZX.Source: §4 · p. 10
• Completeness alone implies that translated ZH rules are derivable, but the paper argues that explicit derivations are needed to show how they follow.It presents those derivations using the algebraic ZX rules.Source: §4 · pp. 11–12

• The authors give a purely algebraic axiomatisation of ZX-calculus using new generators and prove completeness by deriving previously established complete rules.Source: §5 · p. 12
• The axiomatisation supports a simple translation of ZH-calculus diagrams into ZX-calculus and derivation of all ZX-translated ZH rules.Source: §5 · p. 12
• Further work includes proving completeness via a normal form, translating ZX diagrams into ZH-calculus, and applying the algebraic rules to quantum circuit optimisation.Source: §5 · p. 12

Proof of Theorem 3.3

• The proof obtains rules in Figures 2 and 3 from those in Figure 1, deriving them one by one.Source: Proof of Theorem 3.3 · p. 14
• Rules (1a)–(1h) are derived from named axioms and rules, including (S1), (S3), (S2), (EU), (B1), and (B2).The proof also derives (1d) from (S2) and the definition of red spider, then obtains (1e) from (1d) and (S3).Source: Proof of Theorem 3.3 · p. 14

Proposition 5.6

• In Proposition 5.6, rules (2a) and (2c) follow from (S1), (2b) from (S2), and (2f) and (2g) are (Bas0) and (Bas1).The passage also says a rule is obtained by applying a triangle inverse to both sides of (Bas1).Source: Proposition 5.6 · p. 15

Corollary 5.14

• The other part of the Corollary 5.14 proof is established by symmetry.Source: Corollary 5.14 · p. 17
• Rule (2n) is identified with (Pcy).Source: Corollary 5.14 · p. 17
• By (Suc), rule (Zrp) is equivalent to rule (Zero).Source: Corollary 5.14 · p. 18

Proof of Theorem 4.1

• The proof introduces notation for simplicity.Source: Proof of Theorem 4.1 · p. 24

Corollary 5.32

• An induction proof is cited as (L1) in [18], and the ZH rule (BA2) follows from equation 10 and Corollary 5.32.Source: Corollary 5.32 · p. 25

Lemma 5.34

• Proposition 5.37 is titled as a derivation of rule (HS1).Source: Lemma 5.34 · p. 27

Lemma 5.38

• Propositions 5.39, 5.40, and 5.41 are titled as derivations of rules (A), (I), and (O), respectively.Source: Lemma 5.38 · pp. 28–30