セミナー -- Computer Science Seminar
Title
(1) Quantum Logic, Quantum Computation and the Proof Theory of Compact Categories
(2) Complementarity in Categorical Quantum Mechanics
Date
2010年2月12日(金)
(1)10:30より2時間程度
(2)14:45より2時間程度
Room
京都大学理学部3号館(数学教室)305号室
Speaker
Prof. Ross Duncan (Oxford University Computing Laboratory)
Abstract
講演(1)
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.
==================================
講演(2)
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.
==================================
Title
Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages
Date
August 8 (Fri), 2003, 16:00-17:00
Room
Room 115, RIMS, Kyoto University
Speaker
勝股 審也
Abstract
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.