Type-Based Verification of Connectivity Constraints in Lattice Surgery
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912550271057920 |
|---|---|
| author | Wakizaka, Ryo Suzuki, Yasunari Igarashi, Atsushi |
| author_facet | Wakizaka, Ryo Suzuki, Yasunari Igarashi, Atsushi |
| contents | Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed.
This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present $\mathcal{Q}_{LS}$, a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_00529 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Type-Based Verification of Connectivity Constraints in Lattice Surgery Wakizaka, Ryo Suzuki, Yasunari Igarashi, Atsushi Quantum Physics Programming Languages Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed. This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present $\mathcal{Q}_{LS}$, a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem. |
| title | Type-Based Verification of Connectivity Constraints in Lattice Surgery |
| topic | Quantum Physics Programming Languages |
| url | https://arxiv.org/abs/2409.00529 |