Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911979715690496 |
|---|---|
| author | Colledan, Andrea Lago, Ugo Dal |
| author_facet | Colledan, Andrea Lago, Ugo Dal |
| contents | We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including width, depth and gate count, but also variations thereof obtained by considering only some wire types or some gate kinds. The key ingredients for achieving this level of flexibility are effects and refinement types, both relying on indices, that is, generic arithmetic expressions whose operators are interpreted differently depending on the target metric. The approach is shown to be correct through logical predicates, under reasonable assumptions about the chosen resource metric. This approach is empirically evaluated through the QuRA tool, showing that, in many cases, inferring tight bounds is possible in a fully automatic way. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_03121 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages Colledan, Andrea Lago, Ugo Dal Programming Languages Computational Complexity Logic in Computer Science Quantum Physics We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including width, depth and gate count, but also variations thereof obtained by considering only some wire types or some gate kinds. The key ingredients for achieving this level of flexibility are effects and refinement types, both relying on indices, that is, generic arithmetic expressions whose operators are interpreted differently depending on the target metric. The approach is shown to be correct through logical predicates, under reasonable assumptions about the chosen resource metric. This approach is empirically evaluated through the QuRA tool, showing that, in many cases, inferring tight bounds is possible in a fully automatic way. |
| title | Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages |
| topic | Programming Languages Computational Complexity Logic in Computer Science Quantum Physics |
| url | https://arxiv.org/abs/2408.03121 |