Classical Control in Quantum Programs

We present an imperative quantum programming language with physically motivated operational semantics. The language is not restricted to reversible computations, but can be used to describe unitary quantum operations in interaction with measurement and classical control. We are able to model (irreversible) deterministic and probabilistic programs as special cases of quantum programs, in contrast to computational models which assume all quantum operations to be unitary. Due to the presence of loops and conditionals, we have to consider terminating and non-terminating programs. Even with non-terminating programs, it may be of interest to make statements about classical events during the run of the programs like measurement results, contents of classical variables, outputs. For this, we define the notion of classical output, which may already happen before program termination. One application, which would need such classical output, are cryptographic protocols, where we want to define events which must not occur, even in the case of non-terminating protocols.

Programs in our language can contain arbitrary operators and mathematical functions, thus allowing to state very abstract but well-defined specifications and to gradually transform it into programs containing only primitive operations. We also present a simple calculus to transform and reason about programs.

Programs written in pseudo-code can usually easily be transformed into our language, since instructions like "while the measurement on register A does not yield a result satisfying condition P, apply transformation U" have direct counterparts in the formalised language. However, no physically impossible operations (like e.g. cloning) may be expressed.