Optimising Clifford circuits with Quantomatic

Research output: Contribution to journalConference article

Abstract

We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.

Fingerprint

Networks (circuits)

Keywords

  • quantum computation
  • Clifford circuits
  • Quantomatic

Cite this

@article{7dfedbd26ea447e3b0601d1fec15083d,
title = "Optimising Clifford circuits with Quantomatic",
abstract = "We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.",
keywords = "quantum computation, Clifford circuits, Quantomatic",
author = "Andrew Fagan and Ross Duncan",
year = "2019",
month = "1",
day = "29",
doi = "10.4204/EPTCS.287.5",
language = "English",
volume = "287",
pages = "85--105",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",

}

Optimising Clifford circuits with Quantomatic. / Fagan, Andrew; Duncan, Ross.

In: Electronic Proceedings in Theoretical Computer Science, Vol. 287, 29.01.2019, p. 85-105.

Research output: Contribution to journalConference article

TY - JOUR

T1 - Optimising Clifford circuits with Quantomatic

AU - Fagan, Andrew

AU - Duncan, Ross

PY - 2019/1/29

Y1 - 2019/1/29

N2 - We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.

AB - We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.

KW - quantum computation

KW - Clifford circuits

KW - Quantomatic

UR - https://arxiv.org/abs/1901.10114v1

U2 - 10.4204/EPTCS.287.5

DO - 10.4204/EPTCS.287.5

M3 - Conference article

VL - 287

SP - 85

EP - 105

JO - Electronic Proceedings in Theoretical Computer Science

T2 - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

ER -