Proto-Quipper with dynamic lifting

TL;DR

This paper extends Proto-Quipper-M with dynamic lifting, allowing quantum programs to interleave classical and quantum computation by lifting measurement results to influence circuit generation.

Contribution

It introduces Proto-Quipper-Dyn with a new dynamic lifting construct, formalizes its syntax, type system, semantics, and categorical foundation, and demonstrates its use in quantum programming.

Findings

Dynamic lifting enables classical-quantum interleaving.

The type system tracks dynamic lifting with modalities.

Soundness is proven for the semantics.

Abstract

Quipper is a functional programming language for quantum computing. Proto-Quipper is a family of languages aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a construct called dynamic lifting, which is present in Quipper. By virtue of being a circuit description language, Proto-Quipper has two separate runtimes: circuit generation time and circuit execution time. Values that are known at circuit generation time are called parameters, and values that are known at circuit execution time are called states. Dynamic lifting is an operation that enables a state, such as the result of a measurement, to be lifted to a parameter, where it can influence the generation of the next portion of the circuit. As a result, dynamic lifting enables Proto-Quipper programs to interleave classical and quantum computation. We describe the syntax of a language we call Proto-Quipper-Dyn. Its type system uses a system of modalities to keep track of the use of dynamic lifting. We also provide an operational semantics, as well as an abstract categorical semantics for dynamic lifting based on enriched category theory. We prove that both the type system and the operational semantics are sound with respect to our categorical semantics. Finally, we give some examples of Proto-Quipper-Dyn programs that make essential use of dynamic lifting.