Proto-Quipper with Reversing and Control
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916909568491520 |
|---|---|
| author | Fu, Peng Kishida, Kohei Ross, Neil J. Selinger, Peter |
| author_facet | Fu, Peng Kishida, Kohei Ross, Neil J. Selinger, Peter |
| contents | The quantum programming language Quipper supports circuit operations such as reversing and controlling certain quantum circuits. Additionally, Quipper provides a function called with-computed, which can be used to program circuits of the form g; f; g-dagger. The latter is a common pattern in quantum circuit design. One benefit of using with-computed, as opposed to constructing the circuit g ; f; g-dagger directly from g, f, and g-dagger, is that it facilitates an important optimization. Namely, if the resulting circuit is later controlled, only f needs to be controlled; the circuits g and g-dagger need not even be controllable.
In this paper, we formalize a semantics for reversible and controllable circuits, using a dagger symmetric monoidal category R to interpret reversible circuits, and a new notion we call a controllable category N, which encompasses the control and with-computed operations in Quipper. We extend the language Proto-Quipper with reversing, control and the with-computed operation. Since not all circuits are reversible and/or controllable, we use a type system with modalities to track reversibility and controllability. This generalizes the modality of Fu-Kishida-Ross-Selinger 2023. We give an abstract categorical semantics, and show that the type system and operational semantics are sound with respect to this semantics. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_22261 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Proto-Quipper with Reversing and Control Fu, Peng Kishida, Kohei Ross, Neil J. Selinger, Peter Logic in Computer Science Programming Languages Category Theory Quantum Physics The quantum programming language Quipper supports circuit operations such as reversing and controlling certain quantum circuits. Additionally, Quipper provides a function called with-computed, which can be used to program circuits of the form g; f; g-dagger. The latter is a common pattern in quantum circuit design. One benefit of using with-computed, as opposed to constructing the circuit g ; f; g-dagger directly from g, f, and g-dagger, is that it facilitates an important optimization. Namely, if the resulting circuit is later controlled, only f needs to be controlled; the circuits g and g-dagger need not even be controllable. In this paper, we formalize a semantics for reversible and controllable circuits, using a dagger symmetric monoidal category R to interpret reversible circuits, and a new notion we call a controllable category N, which encompasses the control and with-computed operations in Quipper. We extend the language Proto-Quipper with reversing, control and the with-computed operation. Since not all circuits are reversible and/or controllable, we use a type system with modalities to track reversibility and controllability. This generalizes the modality of Fu-Kishida-Ross-Selinger 2023. We give an abstract categorical semantics, and show that the type system and operational semantics are sound with respect to this semantics. |
| title | Proto-Quipper with Reversing and Control |
| topic | Logic in Computer Science Programming Languages Category Theory Quantum Physics |
| url | https://arxiv.org/abs/2410.22261 |