Abstract: |
Familiarity with quantum mechanics will not be assumed
The current methods available for developing quantum algorithms and
protocols are deficient on two main levels. Firstly, they are too
low-level. Quantum algorithms are currently mainly described using the
`network model' corresponding to circuits in classical computation.
One finds a plethora of ad hoc calculations with `bras' and `kets',
normalizing constants, matrices etc. The arguments for the benefits of
a high-level, conceptual approach to designing, programming and
reasoning about quantum computational systems are just as compelling
as for classical computation. Moreover, there is the whole issue of
integrating quantum and classical features, which would surely be
mandatory in any practicable system. At a more fundamental level, the
standard mathematical framework for quantum mechanics is actually
insufficiently comprehensive for informatic purposes: in particular,
the flow of information from quantum to classical arising from
measurements, and the dependence of subsequent stages of the
computation on this information, is not adequately covered by the
standard formalism. As quantum protocols and computations grow more
elaborate and complex, this point is likely to prove of increasing
importance.
In [Abramsky and Coecke 2004] we addressed these
problems, the key ingredient being a categorical axiomatization of
quantum mechanics. The concepts of abstract quantum mechanics are
formulated in any strongly compact closed category with biproducts (of
which the category FdHilb of finite dimensional Hilbert spaces and
linear maps is an example). Preparations, measurements, and classical
data exchange are all morphisms in the category, and their types fully
reflect their kinds. Correctness properties of standard quantum
protocols can be proved at this abstract level. Although this setting
seems purely qualitative, in fact even the Born rule, which specifies
how probabilities are calculated, can be derived. There are also
connections to logic; the calculations in abstract quantum mechanics
can be performed as cut elimination on (possibly cyclic) proof nets;
loops generate scalars (typically, probabilities or probability
amplitudes).
The talk will be in two parts: the first part, given by Abramsky, will
give an overview of our work, and the second part, by Coecke, will
supply more detail, and examine a case study of verifying the
teleportation protocol.
References
J. von Neumann. Mathematische Grundlagen der Quantenmechanik.
Springer-Verlag (1932). English translation in Mathematical Foundations of
Quantum Mechanics. Princeton University Press (1955).
S. Abramsky and B. Coecke. A categorical semantics of quantum
protocols. In the proceedings of LiCS'04 (2004). An extended
version is available at
arXiv:quant-ph/0402130.
|