Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement, the phenomenon in which measurement outcomes of qubits are corre...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2022
|
| Online Access: | https://hdl.handle.net/1721.1/144705 https://orcid.org/0000-0002-4918-4467 |
| _version_ | 1811083243658674176 |
|---|---|
| author | Yuan, Chenhui |
| author2 | Carbin, Michael |
| author_facet | Carbin, Michael Yuan, Chenhui |
| author_sort | Yuan, Chenhui |
| collection | MIT |
| description | Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks.
Programming quantum computers requires awareness of entanglement, the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns.
In this work, I formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation.
I present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification.
I evaluate Twist's type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that several languages disallow, while incurring runtime verification overhead of less than 3.5%. |
| first_indexed | 2024-09-23T12:29:30Z |
| format | Thesis |
| id | mit-1721.1/144705 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T12:29:30Z |
| publishDate | 2022 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1447052022-08-30T03:35:10Z Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs Yuan, Chenhui Carbin, Michael Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement, the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns. In this work, I formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation. I present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification. I evaluate Twist's type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that several languages disallow, while incurring runtime verification overhead of less than 3.5%. S.M. 2022-08-29T16:06:04Z 2022-08-29T16:06:04Z 2022-05 2022-06-21T19:25:56.710Z Thesis https://hdl.handle.net/1721.1/144705 https://orcid.org/0000-0002-4918-4467 In Copyright - Educational Use Permitted Copyright MIT http://rightsstatements.org/page/InC-EDU/1.0/ application/pdf Massachusetts Institute of Technology |
| spellingShingle | Yuan, Chenhui Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs |
| title | Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs |
| title_full | Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs |
| title_fullStr | Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs |
| title_full_unstemmed | Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs |
| title_short | Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs |
| title_sort | twist sound reasoning for purity and entanglement in quantum programs |
| url | https://hdl.handle.net/1721.1/144705 https://orcid.org/0000-0002-4918-4467 |
| work_keys_str_mv | AT yuanchenhui twistsoundreasoningforpurityandentanglementinquantumprograms |