セミナー -- Computer Science Seminar
（１） Quantum Logic, Quantum Computation and the Proof Theory of Compact Categories
（２） Complementarity in Categorical Quantum Mechanics
Prof. Ross Duncan (Oxford University Computing Laboratory)
Quantum Logic, Quantum Computation and the Proof Theory of Compact Categories
Quantum computation has reawakened interest in the underlying logic of quantum mechanics. We briefly examine the "old school" Birkhoff-von Neumann style quantum logic, and discuss why it is not a suitable basis for quantum computation. We then discuss a newer approach, initiated by Abramsky and Coecke and based on a view of logic informed by the Curry-Howard correspondence between proofs and programs. Abstract: Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut elimination procedure is strongly normalising: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as non-logical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.
The main part of this talk is based on book chapter http://arxiv.org/abs/0903.5154.
Complementarity in Categorical Quantum Mechanics
The fundamental feature of quantum mechanics is the existence of incompatible observables. This is usually phrased in a negative way: operators are NOT commuting; the lattice of observables is NON-distributive etc. In this talk I will present the positive content to be found in the existence of complementary quantum observables. We will see that each such pair gives rise to an incredibly rich zoo of algebraic structures all of which can be presented graphically. The resulting graphical language is expressive enough to denote any quantum physical state of an arbitrary number of qubits, and any processes thereof. The rules for manipulating these result in very concise and straightforward computations with elementary quantum gates, translations between distinct quantum computational models, and simulations of quantum algorithms such as the quantum Fourier transform. They enable the description of the interaction between classical and quantum data in quantum informatic protocols. I will describe this formalism in detail, and if time permits explain some applications in the study of measurement based quantum computation and the local hidden variable models. The main part of this talk can be found in http://arxiv.org/abs/0906.4725.
Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages
August 8 (Fri), 2003, 16:00-17:00
Room 115, RIMS, Kyoto University
We extend the study of the relationship between behavioural equivalence and indistinguishability relation to the simply typed lambda calculus, where higher-order types are available. The main technical tool of this study is pre-logical relations, which give a precise characterisation of behavioural equivalence. We establish a relationship between behavioural equivalence and indistinguishability in terms of factorisability. We then consider a higher-order logic to reason about models of the simply typed lambda calculus, and relate the resulting standard satisfaction relation to behavioural satisfaction.