Quantum Expectation Transformers for Cost Analysis

TL;DR

This paper presents a novel expectation transformer framework for analyzing the expected cost and value of classical-quantum programs, supported by formal semantics and applied to well-known quantum algorithms.

Contribution

It introduces a new semantic expectation transformer based on a cost structure, enabling formal analysis of classical-quantum program costs and values.

Findings

Sound and adequate weakest precondition analysis for the language

Formal methods for expected cost and value analysis

Application to quantum algorithms like coin tossing and quantum walks

Abstract

We introduce a new kind of expectation transformer for a mixed classical-quantum programming language. Our semantic approach relies on a new notion of a cost structure, which we introduce and which can be seen as a specialisation of the Kegelspitzen of Keimel and Plotkin. We show that our weakest precondition analysis is both sound and adequate with respect to the operational semantics of the language. Using the induced expectation transformer, we provide formal analysis methods for the expected cost analysis and expected value analysis of classical-quantum programs. We illustrate the usefulness of our techniques by computing the expected cost of several well-known quantum algorithms and protocols, such as coin tossing, repeat until success, entangled state preparation, and quantum walks.