Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages

TL;DR

This work addresses parametric resource estimation for quantum circuit description languages by introducing Proto-Quipper-RA, a type-and-effect system that derives upper bounds on circuit size under multiple metrics. Resource interpretations (CMIs) map abstract operators to concrete metric notions, while resource metric interpretations (RMIs) enable modular, metric-specific reasoning, including both global (e.g., $\text{width}$, $\text{gate count}$) and local (e.g., $\text{depth}$ per wire) measures. Correctness is established via logical relations, showing that type judgments yield sound bounds and that the approach extends to a practical tool, QuRA, which can automatically infer bounds for metrics like width and gate count and apply to algorithms such as the Quantum Fourier Transform. The framework promises flexible, automated resource verification for circuit description languages, with ongoing work to incorporate richer local metrics and denotational semantics. The work emphasizes modularity, enabling new metrics to be added through CMIs/RMIs without reworking the core inference engine, enhancing applicability to heterogeneous quantum hardware constraints.

Abstract

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.

Figures (11)

• Figure 1: An example of quantum circuit: the quantum teleportation circuit
• Figure 2: A Quipper function implementing quantum negation, and the circuit it builds
• Figure 3: A higher-order Quipper function and the result of its application to dumbNot from Figure \ref{['fig:dumbnot']}
• Figure 4: A Quipper function with variable input size, and the circuit it builds on an input of size $n$
• Figure 5: Types and syntax of Proto-Quipper

Theorems & Definitions (14)

• definition 1: Recursive Circuit Metric
• definition 2: Locally Sound CMI
• proposition 1
• definition 3: $\operatorname{\mathit{emit}}$
• definition 4: Local Resource Correctness
• definition 5: Correct Judgment
• definition 6: Correct RMI
• definition 7: Semantic Interpretation of Types
• definition 8: Semantic Interpretation of Typing Contexts
• definition 9: Semantic Well-typedness