Association of Symbolic Logic

Special session on Categorical Logic & Quantum Computation

Speakers, Titles, Abstracts

17 May 2006, afternoon session

Peter Selinger

Idempotents in dagger categories
Abstract: Dagger compact closed categories were recently introduced by Abramsky and Coecke (under the name "strongly compact closed categories") as an abstract presentation of the category of Hilbert spaces and linear maps. I subsequently showed that dagger compact closed categories can also describe "mixed" quantum computation, where the morphisms are completely positive maps. I introduced the CPM construction to pass from the "pure" to the "mixed" world. One slight nuisance with this construction is the following: the category CPM(C) usually does not have biproducts (even if C did), and so one must add them freely to obtain a category CPM+(C) of quantum and classical types. In this talk, I will show that CPM+(C) can be equivalently constructed from CPM(C) by splitting self-adjoint idempotents. I will discuss general properties of idempotents in dagger categories, and comment on the significance of the view that a classical type is given by a self-adjoint idempotent on a quantum type.

Bob Coecke

In the beginning God created tensor.
Abstract: In this talk we show that the part of quantum mechanics relevant to quantum informatics can be fully expressed in terms of tensor structure alone, and, without loss of expressiveness, admits a very high level of abstraction in terms of a particular kind of symmetric monoidal categories. In contrast with the usual Birkhoff-von Neumann lattice-theoretic 'non-logics' this categorical axiomatization comes with some kind of 'hyper-deductive logic', namely a degenerate version of Lambek-Barr-Seely categorical semantics for multiplicative linear logic. Relying on the work of Kelly & Laplaza and Joyal & Street it also follows that such categories admit a purely graphical calculus which turns out to be a quite substantial two-dimensional extension of Dirac's bra-ket calculus.
A first step towards this is the axiomatixation of the tensor product in terms of dagger-compact categories, due to Abramsky (Oxford) & myself, which provides the theory with the notions of scalar, (self-)adjointness, compound system, Bell-states and map-state duality, unitarity, inner-product, trace, positivity, projector, a Born-rule to calculate probabilities, an abstract counterpart to complex phase, and we are in fact able impose the absence of (the redundant) global phases --- the presence of which was the main reason for von Neumann to shift to a lattice-theoretic setting.
Selinger's CPM-construction extends this list with the important notions of mixed states, mixed operations and Jamiolkowski map-state duality.
More surprisingly, also quantum measurements do not need explicit sums and can be defined as a 'self-adjoint' Eilenberg-Moore coalgebra with respect to some particular kind of internal commutative comonoid, a result due to Pavlovic (Kestrel Institute) & myself. In conceptual terms, this definition of measurement exactly captures von Neumann's projection postulate together with the distinct abilities to copy and delete in the quantum world as compared to the classical world (a feature which is key to the whole quantum informatic endeavor). A compelling application of this purely multiplicative notion of quantum measurement, due to Paquette (UdMontreal) & myself, is a simple graphical proof of Naimark's theorem, from which the definition of generalized measurement arises.

Dusko Pavlovic

Bra-ket categories: An elementary language for quantum states (joint work with Bob Coecke)
Abstract: Extending the recent proposals by Abramsky, Coecke and Selinger, we define a simple language of abstract density operators, independent of linear algebra. This provides an elementary interface for some otherwise cumbersome computations, and opens an alley towards nonstandard models of quantum theories.

18 May 2006, afternoon session

Robin Cockett

Programming with classical quantum datatypes
Abstract: The aim of this talk is to describe a method of implementing quantum programming languages based on a "quantum stack". In particular, the manner in which calls to (recursive) functions are managed will be described as will the details of how the stack architecture supports the implementation of datatypes (with classical control) such as list and trees.
A quantum programming language, which compiles down to quantum stack operations, shall be described (and hopefully demonstrated!). The language is based on Peter Selinger's Quantum programming language. However, this language differs somewhat in that it emphasizes the underlying "linear" semantics of the computations and the role of coproducts and datatypes. This makes it is more functional in style (although, of course, it lacks higher order types).
The implementation actually entails a particular semantics and, time permitting, there are some remarks I would like to make on this.
This is joint work with Brett Giles.

Richard Blute

Deep Inference and Probabilistic Coherence Spaces. [Joint work with Prakash Panangaden and Sergey Slavnov]
Abstract: We propose a definition of categorical model of the deep inference system BV. BV was designed as a logical framework for the consideration of Retoré's extension of multiplicative linear logic to include a self-dual noncommutative connective.
Our definition is based on Cockett and Seely's notion of a linear functor. A BV-category is a *-autonomous category with an additional tensor product, which when viewed as a bivariant functor, is linear with a degeneracy condition. We show that this simple definition implies the isomorphisms required of the theory.
We show that coherence spaces, with Retoré's noncommutative tensor, form a model. We then consider Girard's category of probabilistic coherence spaces, and show that it contains an additional monoidal structure making it a BV-category.
We discuss possible applications of such categories to the discrete quantum causal dynamics of Blute-Ivanov-Panangaden. The latter is ongoing work with Guglielmi, Panangaden, and Strassburger.

Sergey Slavnov

"Physical" interpretation of linear logic: semiclassical vs. quantum.
Abstract: It is believed by many researchers that linear logic is somehow related to quantum mechanics. However, various "quantum-mechanical" categories, such as the category of Hilbert spaces, do not seem good for modelling LL, since the two distinct multiplicative conectives both have to be interpreted as tensor product. We consider the symplectic "category" introduced by A. Weinstein for purposes of geometric quantization and related problems. It has classical phase spaces as objects and asymptotic quantum states as morphisms. We note that in this setting a non-degenerate *-autonomous structure arises quite naturally, and this gives us a complete model of MLL. Then we discuss an interpretation of the exponential fragment.

19 May 2006, afternoon session

Nicola Gambino

On relating type-theoretic and category-theoretic interpretations of constructive set theory.
Abstract: Constructive Zermelo-Frankel set theory (CZF) admits both type-theoretic and category-theoretic models. Type-theoretic models were originally introduced by Aczel by defining an interpretation of CZF in Martin-Lof's type theory. Category-theoretic models have been defined by Moerdijk and Palmgren using the techniques of Algebraic Set Theory.
The aim of the talk is to relate these different models of CZF. This will be done exploiting a generalisation of the type-theoretic interpretation of constructive set theories, recently introduced by Aczel and the author.

Claudio Hermida

On modalities induced by categorical relations

Victor Harnik & Michael Makkai

A monadic adjunction between ω-categories and computads
Abstract: An ω-category has objects, called cells, and composition operations in each dimension n < ω, where each (n+1)-cell has a domain and a codomain that are n-cells. The ω-categories form a category ωCat, whose arrows are called ω-functors. For a precise definition, see, e.g. [2].
A computad is an ω-category freely generated by a sequence of indeterminates, or indets (one set of indets in each dimension). A computad map is an ω-functor that preserves indets. The computads with their maps, form a category Comp, a non-full subcategory of ωCat (cf. [2]).
A cell of a computad is, actually, a term that indicates how it was constructed from indets. A computad can be seen as a language for denoting cells in ω-categories. Given an ω-category X, one can build a computad NX, the nerve of X, which has, for each cell of X, an indet of NX denoting it. N:ωCat → ω Comp is a functor that has the inclusion functor I:Comp → ωCat as a left adjoint. The adjoint pair of functors (N,I) shares an important property with familiar adjoint pairs from algebra.
Theorem. The nerve functor N is monadic.
For a definition of monadic (or tripleable) functor, see [1]
REFERENCES
[1] Michael Barr and Charles Wells, Toposes, triples and theories, Grundlehren der Mathematischen Wissenschaften, vol. 278, Springer-Verlag, New York, 1985.
[2] Michael Makkai, The word problem for computads, URL: http://www.math.mcgill.ca/makkai.

Any changes in the program will be reflected here as necessary - but for official information please visit the official conference page.