Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916657331437568 |
|---|---|
| author | Sundaram, Aarthi Rand, Robert Singhal, Kartik Lackey, Brad |
| author_facet | Sundaram, Aarthi Rand, Robert Singhal, Kartik Lackey, Brad |
| contents | 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 $T$-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 $T$ gates necessary to perform a multiply-controlled $Z$ gate. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2101_08939 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs Sundaram, Aarthi Rand, Robert Singhal, Kartik Lackey, Brad Quantum Physics Emerging Technologies Logic in Computer Science Programming Languages F.3.1; D.2.4; F.4.1; I.1.1 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 $T$-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 $T$ gates necessary to perform a multiply-controlled $Z$ gate. |
| title | Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs |
| topic | Quantum Physics Emerging Technologies Logic in Computer Science Programming Languages F.3.1; D.2.4; F.4.1; I.1.1 |
| url | https://arxiv.org/abs/2101.08939 |