RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
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_ | 1866909977339232256 |
|---|---|
| author | Matsushita, Yusuke Hirata, Kengo Wakizaka, Ryo D'Osualdo, Emanuele |
| author_facet | Matsushita, Yusuke Hirata, Kengo Wakizaka, Ryo D'Osualdo, Emanuele |
| contents | Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement, and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL, which is able to soundly reduce reasoning about superposition states to reasoning about pure states (basis-locality), and reasoning about mixed states arising from measurement to reasoning about pure states (outcome-locality). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_23472 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing Matsushita, Yusuke Hirata, Kengo Wakizaka, Ryo D'Osualdo, Emanuele Programming Languages Logic in Computer Science Quantum Physics Quantum Separation Logic (QSL) has been proposed as an effective tool to improve the scalability of deductive reasoning for quantum programs. In QSL, separation is interpreted as disentanglement, and the frame rule brings a notion of entanglement-local specification (one that only talks about the qubits entangled with those acted upon by the program). In this paper, we identify two notions of locality unique to the quantum domain, and we construct a novel quantum separation logic, RapunSL, which is able to soundly reduce reasoning about superposition states to reasoning about pure states (basis-locality), and reasoning about mixed states arising from measurement to reasoning about pure states (outcome-locality). To do so, we introduce two connectives, linear combination and mixing, which together with separation provide a dramatic improvement in the scalability of reasoning, as we demonstrate on a series of challenging case studies. |
| title | RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing |
| topic | Programming Languages Logic in Computer Science Quantum Physics |
| url | https://arxiv.org/abs/2511.23472 |