Transcript while (M) P

Classical Control in
Quantum Programs
Dominique Unruh
IAKS, Universität Karlsruhe
Founded by the European Project ProSecCo IST-2001-39227
Design Goals
• Quantum programming language
We present a method of modelling a quantum programming language in a way that should allow to
write quantum programs in a formal way, without loosing the similarity to pseudo-code which is
essential for an intuitive approach to algorithms.
• Terminating and non-terminating
Our modelling shall support the design of terminating as well of non-terminating programs within the
same mathematical framework.
• Mixed classical and quantum operations
We want to be able to represent both pure quantum (unitary) as well as classical operations
(measurements, erasure) using the same framework. That is, we do not impose a strict separation
between a classical controlling computer and the controlled quantum registers.
• Output during the program’s run
We show how to model programs which give classical (i.e. measured) output during the program’s
run. This is especially useful, if the programs in consideration do not terminate but give a
continuous stream of results, since the usual run-and-then-measure-after-termination approach is
not sensible in that case.
• Physical interpretation
A programs behaviour can be modelled as a measurement process (with defined resulting state in case
of termination). In order to avoid artificial constructions we adhere to these operational semantics
and show how to transform any program into the mathematical description of a measurement
process.
Operational Semantics
• A program is a physical experiment
The process of running a program is very much comparable to performing a physical experiment: At
the beginning, the machine is in a given initial state. Then this state is modified by performing
various operations. These may include measurements during the experiment (outputs of the
program). The experiment possibly terminates (real life experiments always do, due to limited
resources, programs not necessarily). If the program terminates, the machine afterwards is in a
well-defined post-measurement state.
• A physical experiment is a measurement
Any physical experiment can be seen as a measurement operation. We distinguish two kinds: a
measurement operation defining the post-measurement state (called general measurement or
PMVM), and a measurement not defining the post-measurement state (a POVM). To describe
measurements which may or may not have a post-measurement state, we need to use the convex
combination of a general measurement and a PMVM. This combination we will call a mixed
measurement.
• A program is a measurement
Since we can consider a program as an experiment, and an experiment as a mixed measurement, it is
natural to model a program as a mixed measurement. The outputs of the program are
measurement results and are finite or infinite sequences over an alphabet Σ. This gives rise to
operational semantics of programs, which are simply mathematical descriptions of measurements.
• Classical, measurement, unitary operations
The mixed measurement formalism is strong enough to have as special cases classical (probabilistic)
programs, orthogonal measurements, and unitary operations, thus capturing all kinds of
operations in a single mathematical framework.
Composing programs
• Sequentially execute several programs
If two programs P and Q are defined, the composed program P;Q can be interpreted as first
executing P (yielding some output), and then—if P terminated—executing Q on the postexecution state of P. The output of the composed program is then given by the concatenation of
the respective inputs.
Examples
P;Q
Run P then run Q
{P;Q};R
P;{Q;R}
Composition is associative, so these
three are equal
P;Q;R
print x; print y
Outputs xy
Print-Command
• Any outputs can be build up from constant outputs
By defining an elementary program print x, one can build up any output by using switch (see
below). E.g. switch (M as m) print m outputs the result of measurement M.
• Constant outputs are constant measurements
The program print x outputting x is simply a measurement with constant outcome x and which
does not modify the programs state.
Examples
print a; print b
Equivalent programs outputting ab
print ab
switch (M as m) print m
print M
Outputs result of measuring M.
(shorthand)
while (true) print x
Outputs infinite sequence x∞
Branching (if/switch)
• Branching as classical control
In our modelling we consider branching which is conditional upon the outcomes of measurements.
This is opposed to controlled unitary transformation (e.g. CNOT), where the controlling qubit is
not measured. More complex quantum algorithms usually have such classical control, be it an
overall loop repeating the experiment until a useful result is obtained (e.g. a non-trivial factor in
Shor’s factoring algorithm).
• Branching programs are composed measurements
A program if (M) P can be interpreted as the experiment measuring M and then executing the
program P if M yielded the outcome true. This experiment can be expressed as a measurement
in a straightforward manner: if Mi denotes the superoperator describing the post-measurement
state on outcome i, then if (M) P is simply defined as PMtrue+Mfalse. Analogously we
define if (M) P else Q.
• More powerful: the switch-statement
An if-statement can only distinguish between two cases: true and false. In many cases a more
powerful statement, the switch statement. switch (M as m) P(m) measures M and then
executes the program P(m) where m is the outcome of the measurement.
Examples
if (M) P else Q
Measure M, if true, run P otherwise Q
switch (M as m)
print m^2
print M^2
Outputs the square of the result of
measuring M.
(shorthand)
switch (M as m) {
case m=1: print “one”
case m>1: print “many”
}
Measure M, output one or many,
depending of the outcome
Loops
•
Informal description simple
The program while (M) P denotes the experiment of repeatedly measuring M and if the outcome
is true then executing P. If the outcome is false, abort.
•
Mathematical description turns out to be difficult
Two approaches immediately come to mind for defining while. The first would be to define while
as a least fixed point. However due to the possibility of outputs there is no natural lattice
structure. The second would be to define while as the limit of
if(M){P;if(M){P;...}}. However, there is no natural topology giving the desired
results.
•
Axiomatic approach
Since a direct limit/fixed point approach fails, we define while (M) P by stating some properties
the experiment above should fulfill. These axioms can informally be stated as follows:
•
The loop runs n times and terminates, iff M yields n times true and then false, and if P
terminates n times.
•
The loop runs n times and does not terminate, iff M yields n times true, and if P terminates
n–1 times and does not terminate the n-th time.
•
The loop runs an infinite number of times, iff always M yields true, and if P always
terminates.
•
The probability that one of these events occurs is 1.
It can be shown that there is exactly one program (i.e. mixed measurement) exists fulfilling these
axioms.
Examples
while (M) P
Run program P while measurement M
yields true.
while (M) print N
Measure M. If nonzero, measure N,
output the outcome, and redo from start
Reasoning about programs
• Conditions are sets of states
Modelling a pre-/postcondition as a set of states (density operators) gives as the ability to express
even complex conditions like “variable x contains an uniform random value” or “variables x and
y are unentangled” or “variable x is in the computational basis”.
• Pre-/postconditions
If for any state ρ in M, the program P takes ρ to a state in N, we write {M} P {N}
• Conditional equivalence of programs
If two programs P, Q behave identically upon a given set M of initial states, we say they are
equivalent on M, written {M} P = Q.
• Programs can be conditioned on outputs
If P is a program possibly having output a, we can define P|a as the program P restricted to having
output a. Note that P|a is not probability preserving.
Examples
{1} P {1}
If the initial state is a random state, so
is the post-execution state (e.g. P is a
permutation of basis states)
{x in computational basis}
P=noop
If variable x is in the computational
basis, program P has no effect (e.g. P
might be a dephasing of x)
{tr ρ = 1} P|a { tr ρ=½}
Program P has probability ½ of
outputting a