Expectation-based Analysis of Higher-Order Quantum Programs
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915748425760768 |
|---|---|
| author | Avanzini, Martin Díaz-Caro, Alejandro Hainry, Emmanuel Péchoux, Romain |
| author_facet | Avanzini, Martin Díaz-Caro, Alejandro Hainry, Emmanuel Péchoux, Romain |
| contents | The paper extends the expectation transformer based analysis of higher-order probabilistic programs to the quantum higher-order setting. The quantum language we are considering can be seen as an extension of PCF, featuring unbounded recursion. The language admits classical and quantum data, as well as a tick operator to account for costs. Our quantum expectation transformer translates such programs into a functional, non-quantum language, enriched with a type and operations over so called cost-structures. By specializing the cost-structure, this methodology makes it possible to study several expectation based properties of quantum programs, such as average case cost, probabilities of events or expected values, in terms of the translated non-quantum programs, this way enabling classical reasoning techniques. As a show-case, we adapt a refinement type system, capable of reasoning on upper-bounds. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_18441 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Expectation-based Analysis of Higher-Order Quantum Programs Avanzini, Martin Díaz-Caro, Alejandro Hainry, Emmanuel Péchoux, Romain Logic in Computer Science The paper extends the expectation transformer based analysis of higher-order probabilistic programs to the quantum higher-order setting. The quantum language we are considering can be seen as an extension of PCF, featuring unbounded recursion. The language admits classical and quantum data, as well as a tick operator to account for costs. Our quantum expectation transformer translates such programs into a functional, non-quantum language, enriched with a type and operations over so called cost-structures. By specializing the cost-structure, this methodology makes it possible to study several expectation based properties of quantum programs, such as average case cost, probabilities of events or expected values, in terms of the translated non-quantum programs, this way enabling classical reasoning techniques. As a show-case, we adapt a refinement type system, capable of reasoning on upper-bounds. |
| title | Expectation-based Analysis of Higher-Order Quantum Programs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.18441 |