Expectation-based Analysis of Higher-Order Quantum Programs
Martin Avanzini, Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux
TL;DR
The paper addresses the challenge of analyzing higher‑order quantum programs by extending expectation transformers to the quantum setting. It introduces a CPS‑based transformation from a universal quantum language to a cost‑structure language built on Kegelspitzen, enabling formal reasoning about expected costs and values. A refinement‑type system is then used to derive sound upper bounds for these expectations, demonstrated on quantum cointossing, higher‑order quantum cointossing, and Grover search. The approach provides a compositional, classical reasoning framework for quantitative properties of quantum programs and lays the groundwork for automated analysis. This work broadens the toolkit for resource and performance analysis in quantum programming languages, with potential applications to compiler analyses and resource‑aware quantum software development.
Abstract
The paper extends the expectation transformer based analysis of higher-order probabilistic programs to the quantum higher-order setting. The quantum language we are considering can be seen as an extension of PCF, featuring unbounded recursion. The language admits classical and quantum data, as well as a tick operator to account for costs. Our quantum expectation transformer translates such programs into a functional, non-quantum language, enriched with a type and operations over so called cost-structures. By specializing the cost-structure, this methodology makes it possible to study several expectation based properties of quantum programs, such as average case cost, probabilities of events or expected values, in terms of the translated non-quantum programs, this way enabling classical reasoning techniques. As a show-case, we adapt a refinement type system, capable of reasoning on upper-bounds.