Encoding High-level Quantum Programs as SZX-diagrams
summary
Method encodes a bounded fragment of Proto-Quipper-D into Scalable ZX-diagram families by translating type judgments into diagram templates; vectors become cable multiplicities, list instantiation replicates a subdiagram per element, and conditionals become diagram splits with empty-wire cases. Resulting SZX families implement examples like controlled rotations and QFT while keeping linear growth in diagram size (rather than the usual O(n^2) gate blowup). Limitations: no recursion so only terminating programs are supported, and soundness proofs remain to be completed.
AI-written summary · about
chapters (5)
- 0:00Encoding quantum programs
- 2:27Calculus as intermediate
- 6:04Lambda_d to SZX diagrams
- 12:27Algorithm translation and QFT example
- 15:41Advantages and future work
related talks
31mQuantum compilation using the ZX calculus
23mFrom Fermions to Qubits: A ZX-Calculus Perspective
14mHybrid quantum-classical circuit simplification with the ZX-calculus
30mDependently Typed Quantum Programming in Proto-Quipper
49mFrom ZX to first order logic: a survey of string diagrammatic calculi
32mFault tolerance with the ZX-calculus and fusion complexes: tools for QEC development in the...
20mHybrid Quantum-Classical Machine Learning with String Diagrams
16mCompiling and Running High-level Quantum Programs