Resource-Aware Hybrid Quantum Programming with General Recursion and Quantum Control

TL;DR

This work tackles the challenge of static, resource-aware analysis for hybrid quantum programs with general recursion. It introduces $Hyrql$, a language that combines classical control with quantum data via a shape operator, and provides a semantics-preserving translation to Simply-Typed Term Rewrite Systems to leverage ICC techniques for termination and complexity. Key contributions include a full type system and operational semantics with standard properties (subject reduction, progress, confluence), undecidability results for orthogonality in the full language, a translation algorithm TranslateEntry linking to STTRS with semantic preservation and complexity relations, and illustrative examples such as Hadamard, quantum switch, BB84, map, and Ackermann. The framework enables resource-aware design of variational and other hybrid quantum algorithms by enabling reuse of established TRS tools to bound resources in quantum circuits.

Abstract

This paper introduces the hybrid quantum language with general recursion $\mathtt{Hyrql}$, driven towards resource-analysis. By design, $\mathtt{Hyrql}$ does not require the specification of an initial set of quantum gates and, hence, is well amenable towards a generic cost analysis. Indeed, languages using different sets of quantum gates lead to representations of quantum circuits whose complexity varies. Towards resource-analysis, a semantics-preserving compilation algorithm to simply-typed term rewrite systems is described; allowing a generic reuse of all known techniques for analyzing the complexity of term rewrite systems. We prove the versatility of this approach through many examples.