Quantum Logic Inspired by Quantum Computation

A workshop held at Indiana University

May 11-12, 2009

9:00 AM - 5:30 PM

The workshop schedule is now available.

Our aim is to organize a small workshop that would bring together people who are developing new areas of logic coming from quantum computation, and also people who are interested in related projects coming from areas of philosophical logic, mathematics, and theoretical computer science.
Our workshop will be held on Monday and Tuesday, May 11-12, 2009.

Monday's sessions will be in Lindley Hall 102, and Tuesday's in LH 101.

The sessions are open to the public.


Michael Dunn, Indiana University

Larry Moss, Indiana University

Zhenghan Wang, Microsoft Station Q


IU Department of Mathematics

IU Program in Pure and Applied Logic

IU School of Informatics

National Science Foundation

Speakers/Titles/Abstracts/Related Papers

Samson Abramsky (Oxford University Computing Laboratory): Categorical Quantum Mechanics

We introduce the categorical approach to quantum mechanics which we have developed with Bob Coecke and others in our group at Oxford. This provides an effective setting for quantum information and computation. We also discuss the connections to logic, and show how No-Cloning and related results can be recast in logical terms in the setting of categorical logic.

Categorical Quantum Mechanics (with Bob Coecke) This paper has appeared in Handbook of Quantum Logic and Quantum Structures: Quantum Logic, ed. K. Engesser, D. Gabbay and D. Lehmann, pages 261--324, Elsevier 2009.

No-Cloning In Categorical Quantum Mechanics. This paper is to appear in Semantic Techniques in Quantum Computation, ed. S. Gay and I. Mackie, Cambridge University Press 2009.

Alexandru Baltag (Oxford University Computing Laboratory): The Logic of Quantum Actions in Compound Systems

I will bring together the two parts presented in Sonja Smets’ talk and use the formalism of Dynamic-Epistemic logic to model and reason about the non-local informational dynamics triggered by quantum observations (measurements) and un-observed evolutions (quantum gates) in compound quantum systems. We show how this combined logical formalism expresses important features of quantum measurements and unitary evolutions of multi-partite states, and we give logical characterizations to various forms of entanglement (e.g. the Bell states, the GHZ states etc). As applications, we use our logic to give formal correctness proofs for at least one of the following protocols (Teleportation, Quantum Secret Sharing protocol, Superdense Coding, Quantum Key Distribution etc.). In the remainder of this talk I will show how our formalism can be extended to model how classical agents (seen as classical subsystems) record the results of their quantum observations and perform actions. The goal is to model all aspects of the classical-quantum interaction present in the mentioned quantum protocols: this includes the memory of classical agents, classical communication and classical “control” (indicating the fact that agents may have access to some parts of a quantum sytem but not to others). This presentation covers developments arising from our work in the two papers below on the dynamic logic of entanglement.

LQP: The Dynamic Logic of Quantum Information (with Sonja Smets), Mathematical Structures in Computer Science, 16, 2006.

A Dynamic-Logical Perspective On Quantum Behavior (with Sonja Smets), Studia Logica 89, 2006.

Jeffrey Bub and Allen Stairs (University of Maryland): Contextuality and Nonlocality in ‘No Signaling’ Theories

Recently, there has been a good deal of interest in so-called ‘PR-boxes’ - hypothetical devices that allow for nonlocal correlations stronger than quantum mechanical correlations, but that don't permit superluminal signaling. We will describe a particular class of nonlocal boxes that we call 'KS-boxes' (because of their relationship to examples from Kochen and Specker and Klyachko.) These boxes exhibit a range of correlations that raise interesting issues about the relationship between nonlocality and contextuality. In particular, they include cases that are no more nonlocal than classical boxes, but that can't be simulated classically or quantum mechanically. We also consider how best to represent the logical structure of devices of this sort. We propose partial Boolean algebras as a candidate worth considering, and we look at how the differences between products of partial Boolean algebras and products of lattices could help shed light on the differences between quantum-mechanical EPR-type correlations and the correlations of PR boxes and KS boxes.

Contextuality and Nonlocality in ‘No Signaling’ Theories

Bob Coecke (Oxford University Computing Laboratory): Quantum Picturalism

We report on progress in an approach which aims to provide quantum theory with a purely diagrammatic calculus, a logical foundation, and increased degrees of axiomatic freedom, while still retaining full expressiveness. Key to this approach is the fact that monoidal categories provide a natural framework to reason about systems, processes and their interactions of any kind. We provide two applications of this framework. An axiomatization of the notion of complementary observables exposes the flows of information in sophisticated quantum informatic protocols involving complex entanglements, and an axiomatization of relative phases provides new insights in the origin and peculiarity of quantum non-locality.

Kindergarten quantum mechanics

Introducing categories to the practicing physicist

Latest results, on which I will try to focus in the talk:

Interacting quantum observables (with Duncan, in ICALP'08)

The group-theoretic origin of non-locality (with Edwards and Spekkens)

Survey paper for the journal Contemporary Physics entitled “Quantum picturalism”, Draft March 1st.

Maria Luisa Dalla Chiara (University of Florence) and Roberto Giuntini (University of Cagliari):

(1) Sharp and approximate quantum computational logics (abstract), and

(2) Algebraic characterizations of quantum computational logics (abstract).

Logics from Quantum Computation (with Roberto Leporini)

Compositional and Holistics Quantum Computational Semantics (with Roberto Leporini)

Stan Gudder (University of Denver): Quantum Measure Theory slides

Quantum measure theory was initiated by R. Sorkin in 1994 as an outgrowth of his studies on the histories approach to quantum mechanics and quantum gravity. We begin by defining a quantum measure space and presenting some examples. We discuss why quantum interference requires us to generalize classical measure theory. We consider compatibility of events and the center of a quantum measure space relative to a quantum measure. We then discuss a characterization of quantum measures in terms of signed product measures. We next define a quantum integral and discuss some of its properties.

Quantum Measure Theory

Finite Quantum Measure Spaces

Tobias Hagge (UT Dallas): Quantum Logic on finite dimensional Hilbert spaces slides

The subspaces of a finite dimensional Hilbert space form a modular ortholattice, and have additional nice properties. The extra structure has consequences in the Birkhoff-Von Neumann propositional quantum logic of a finite dimensional Hilbert space. For instance, the logic is decidable (which is not true with a general modular lattice), and the set of tautologies one obtains depends on the dimension of the underlying Hilbert space. I'll discuss these and related phenomena and possible connections to quantum computing.

John Harding (New Mexico State University): Orthomodularity and decompositions

Orthomodularity arises from consideration of the closed subspaces of a Hilbert space, and it was long thought that orthomodularity was closely tied to the Hilbert space structure. This is not the case. The closed subspaces of a Hilbert space correspond to direct product decompositions of the space, and the direct product decompositions of most familiar objects form orthomodular structures. This holds in particular for sets, groups, topological spaces, and so forth.

The connection between orthomodularity and direct product decompositions is used to build an axiomatic system for experimental systems. Further, by their nature, direct product decompositions are creatures of an essentially categorical nature. This allows one to construct orthomodular structures from decompositions of abstract objects in quite general categories. In particular, categories currently considered in categorical approaches to quantum computation allow this approach. This yields a bridge between these newer categorical approaches and the quantum logic.

Axioms of an Experimental System

A link between quantum logic and categorical quantum mechanics

Prakash Panangaden (McGill University): Proof Nets and Formal Feynman Diagrams

I will describe a formal connection between proof nets in linear logic and Feynman diagrams. We introduce a calculus, the phi-calculus, which is inspired by Feynman diagrams in quantum field theory. The ingredients are formal integrals, formal power series, a derivative construct and analogues of the Dirac delta function.

Many of the manipulations of proof nets can be understood as manipulations of formulas reminiscent of a beginning calculus course. In particular the "box" behaves like an exponential. All the equations for MELL (multiplicative-exponetial linear logic) hold (but I will not prove that in the talk). I will end with some speculations about Feynman diagrams.

Proof Nets and Formal Feynman Diagrams (with Richard Blute)

Amr Sabry (Indiana University): Expressing Quantum Computations in the Arrow Calculus

We show that the model of quantum computation based on density matrices and superoperators can be decomposed in a pure classical (functional) part and an effectful part modeling probabilities and measurement. The effectful part can be modeled using a generalization of monads called arrows. We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework expresses quantum programming using well-understood and familiar classical patterns for programming in the presence of computational effects. In addition, the five laws of the arrow calculus provide a convenient framework for equational reasoning about quantum computations that include measurements.

The arrow calculus as a quantum programming language (with Juliana Kaizer Vizzotto and Andre Rauber Du Bois)

Structuring Quantum Effects: Superoperators as Arrows (with Juliana Kaizer Vizzotto and Thorsten Altenkirch)

Sonja Smets (University of Groningen): Dynamic and Epistemic Perspectives on Quantum Behavior

My talk consists of two parts, representing the recent and on-going joint work with A. Baltag in the papers below. First I will concentrate on an improvement of the older results (due to Piron, Soler, Mayet and others) on the Hilbert-complete axiomatizations of algebraic quantum logic and present a dynamic-logical setting, in which physical actions (and not only static physical properties) are logically represented. Secondly I will focus on compound systems and analyse both classical and quantum correlations. Our formalism for these correlations is based on an extension of epistemic logic with operators for “group knowledge”. As models we introduce correlation models, as a generalization of the “interpreted systems” semantics (commonly used in Computer Science as a model for information flow in distributed systems). We use this second setting to investigate the relationship between the information carried by each of the parts of a complex system and the information carried by the whole system. While our dynamic logical setting explains the non-local informational dynamics of quantum systems that are triggered by quantum observations (measurements) and un-observed evolutions (quantum gates), the epistemic logical setting yields an informational-logical characterization of the notion of “quantum entanglement”.

Complete Axiomatizations for Quantum Actions, (with Alexandru Baltag) International Journal of Theoretical Physics, 44, 2005.

Correlated Information: A Logic for Multi-Partite Quantum Systems (with Alexandru Baltag) (n B. Coecke and P. Panangaden (eds.) Proceedings of the 6th Workshop on Quantum Physics and Logic, ENTCS, 2009.

Zhenghan Wang (Microsoft Station Q): Topological Quantum Computing slides
Alex Wilce (Susquehanna University): Symmetry and composition in probabilistic theories

Both classical and quantum mechanics offer a standard device wherewith to combine physical systems: the Cartesian product in the former case, and the Hilbert space tensor product in the latter. In more general probabilistic theories, however, one finds a spectrum of different “non-signaling" products, bounded by a maximal product allowing entangled states but no entangled effects, and a minimal product allowing entangled effects but no entangled states. If we are aiming to understand QM, we surely want to account for the existence of a single, canonical product affording both kinds of entanglement. In this talk, I describe a recipe for building probabilistic theories having strong symmetry properties, using as data any uniform method for extending the symmetry group of a classical system (here: the symmetric group of a set) to a larger group. Subject to some plausible conditions, this construction leads to a symmetric monoidal category, in which the product is non-signaling. There is no guarantee that the composite systems obtained in this way will support arbitrary product states; however, when this desideratum is met, good things follow.

Symmetry and composition in probabilistic theories

Teleportation in general probabilistic theories (with H. Barnum, J. Barrett, and M. Leifer)

Symmetry and topology in quantum logic

Noson Yanofsky (Brooklyn College): A Classification of Hidden-Variable Properties slides

Hidden variables are extra components added to try to banish counterintuitive features of quantum mechanics. We start with a quantum-mechanical model and describe various properties that can be asked of a hidden-variable model. We present six such properties and a Venn diagram of how they are related. With two existence theorems and three no-go theorems (EPR, Bell, and Kochen-Specker), we show which properties of empirically equivalent hidden-variable models are possible and which are not. Formally, our treatment relies only on classical probability models, and physical phenomena are used only to motivate which models to choose. We conclude with a discussion of what possible effects hidden variables might have on quantum computation.

A Classification of Hidden-Variable Properties (with Adam Brandenburger)