2021/01/22 by Aarthi Sundaram, Sundaram, Aarthi, Robert Rand +8 · 2 voices · 4 citations
Computer Science · Engineering · Physics and Astronomy · #Computability, Logic, AI Algorithms #Low-power high-performance VLSI design #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography #Quantum Mechanics and Applications
paper · pdf · doi:10.48550/arxiv.2101.08939
openalex created_date 2022/07/25 · openalex publication_date 2026/07/23 · openalex updated_date 2026/08/03
We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bipartition, (iii) checking the transversality of a gate with respect to a given stabilizer code, and (iv) computing post-measurement states for computational basis measurements. Further, this logic is extended to accommodate universal quantum computing by deriving Hoare triples for the <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>T</mml:mi> </mml:math> -gate, multiply-controlled unitaries such as the Toffoli gate, and some gate injection circuits that use associated magic states. A number of interesting results emerge from this logic, including a lower bound on the number of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>T</mml:mi> </mml:math> gates necessary to perform a multiply-controlled <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>Z</mml:mi> </mml:math> gate.