Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages

TL;DR

This paper presents a flexible type system for Quipper that estimates upper bounds on quantum circuit sizes across various metrics, using effects and refinement types, and demonstrates its effectiveness with the QuRA tool.

Contribution

It introduces a novel type system with effects and refinement types for resource estimation in quantum circuits, enabling automatic and flexible size bounds.

Findings

Effective automatic inference of tight bounds in many cases

Flexible estimation across multiple resource metrics

Validated approach through empirical evaluation with QuRA

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.