## セミナー -- Computer Science Seminar

Title

**
（１） Quantum Logic, Quantum Computation and the Proof Theory of Compact Categories
（２） Complementarity in Categorical Quantum Mechanics
**

Date

２０１０年２月１２日（金）

（１）１０：３０より２時間程度

（２）１４：４５より２時間程度

Room

京都大学理学部３号館（数学教室）３０５号室

Speaker

Prof. Ross Duncan (Oxford University Computing Laboratory)

Abstract

講演（１）

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.

==================================

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.