Amsterdam Quantum Logic Workshop

---

Abstract: It is now exactly 75 years ago that John von Neumann denounced his own Hilbert space formalism: ``I would like to make a confession which may seem immoral: I do not believe absolutely in Hilbert space no more.'' (sic) [1] His reason was that Hilbert space does not elucidate in any direct manner the key quantum behaviors. One year later, together with Birkhoff, they published "The logic of quantum mechanics". However, it is fair to say that this program was never successful nor does it have anything to do with logic. So what is logic? We will conceive logic in two manners: (1) Something which captures the mathematical content of language (cf `and', `or', `no', `if ... then' are captured by Boolean algebra); (2) something that can be encoded in a `machine' and enables it to reason.

Recently we have proposed a new kind of `logic of quantum mechanics'. It follows Schrodinger in that the behavior of compound quantum systems, described by the tensor product [2, again 75 years ago], that captures the quantum behaviors. Over the past couple of years we have played the following game: how much quantum phenomena can be derived from `composition + epsilon'. It turned out that epsilon can be taken to be `very little', surely not involving anything like continuum, fields, vector spaces, but merely a `two-dimensional space' of temporal composition (cf `and then') and compoundness (cf `while'), together with some very natural purely operational assertion. In a very short time, this radically different approach has produced a universal graphical language for quantum theory [5, 6] which helped to resolve some open problems.

Most importantly, it paved the way to automate quantum reasoning [3], and also enables to model meaning for natural languages [4]. That is, we are truly taking `quantum logic' now! If time permits, we also discuss how this logical view has helped to solve concrete problems in quantum information.

A written down version of this talk is [7].

[1] M. Redei, ``Why John von Neumann did not like the Hilbert space formalism of quantum mechanics (and what he liked instead)'', Stud Hist Phil Mod Phys 27, 1997, 493-510.

[2] E. Schroedinger, ``Discussion of probability relations between separated systems'', Proc Camb Phil Soc 31 and 32, 1935 and 1936, 555-563 and 446-451.

[3] New scientist, ``Quantum links let computers read'', 11 Dec.~2011.

[4] Quantomatic, https://sites.google.com/site/quantomatic/

[5] B. Coecke, ``Quantum picturalism'', Contemporary Physics 51, 2010, 59-83.

[6] B. Coecke and A. Kissinger, ``Picturing Quantum Processes'', Cambridge UP, forthcoming.

[7] B. Coecke, ``The logic of quantum mechanics - take II'', arXiv:1204.3458

---

Slides: pdf

---

Abstract: Much about a quantum system is captured by the collection of its classical subsystems, such as algebraic, logical, and information-theoretic aspects. However, one can rigorously prove that the collection of classical subsystems cannot capture all information about a quantum system, for which more structure has to be added. This question is answered by the notion of an active lattice, which adds the information of how to switch between two classical viewpoints. After a survey of this area, I will discuss how to characterise active lattices, and how to reconstruct an operator algebra from its active lattice.

---

Slides: pdf

---

Abstract: The development of the theory of categories enriched in a monoidal category V has, since its inception, been motivated by a particularly simple example: putting (V,⊗,I)=([0,∞]^op,+,0) one gets metric space theory [Lawvere, 1973]. A so-called partial metric space [Matthews, 1994] is a sort of metric space in which ``the distance from a point to itself may be non-zero''. I will show that such partial metric spaces are enriched categories too---but now enriched in a bicategory W. In fact, the appropriate bicategory W is obtained as a universal construction on [0,∞], most easily explained in terms of `diagonals'. There is a logical aspect to all this work: precisely as V-categories relate to multi-valued logic, W-categories relate to multi-typed and multi-valued logic. It is this extra degree of freedom -- the many possible types -- that allow for an elegant treatment of `partialness'. The case of sheaves (`sets of partially defined elements') will further illustrate this point.

---

Abstract: Recent reconstructions of finite-dimensional quantum theory employ strong axioms that immediately rule out the theory's real and quaternionic variants. Even so, they are hard slogging. In this talk, I will sketch a much quicker and more comfortable route to the vecinity of standard QM.

More specifically, I derive from a few simple postulates, and in a conspicuously easy way, a representation of finite-dimensional probabilistic systems in terms of homogenous, self-dual order-unit spaces (arXiv 1206.2897). The Koecher-Vinberg Theorem identifies such spaces with euclidean Jordan algebras; these, in turn, have a well-known classification as direct sums of real, complex and quaternionic quantum systems, the exceptional Jordan algebra, and spin factors --- ``bits" having the structure of n-dimensional balls. A key idea is to pair every system with an isomorphic conjugate system, by means of a state perfectly and uniformly correlating every basic measurement on the first system with its counterpart on the second. (In QM, the conjugate of a system with Hilbert space H is the one associated with the conjugate Hilbert space H, and the special state is the maximally entangled ``EPR" state on H ⊗ H.)

I will also discuss some recent (arXiv:1202.4513) and on-going work with Howard Barnum and Matthew Graydon, in which we construct a symmetric monoidal category of such systems, thus obtaining a non-signaling probabilistic theory that harmoniously combines real, complex and quaternionic QM, while allowing for just a little bit more generality.

---

Slides: pdf

---

Abstract: Floyd-Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd-Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.

---

Slides: pdf

---

Abstract: The goal of position-based cryptography is to use the geographic position of a party as its sole credential. A central building block is the task of position-verification where a prover wants to convince a set of verifiers that she is at a certain geographical location. Protocols typically assume that messages can not travel faster than the speed of light. By responding to a verifier in a timely manner one can guarantee to be within a certain distance of that verifier.

In this talk, I will present a not very well-known form of quantum teleportation called port-based teleportation. Using this form of teleportation, one can perform non-local quantum computation and thereby break any quantum scheme for position verification.

In the last part, I will present a mechanical abstraction of quantum teleportation called the garden-hose model for computing a Boolean function. This model serves as stepping stone to understanding teleportation attacks on simple quantum protocols for position verification.

---

Slides: pptx

---

Abstract: Probabilistic Logic of Quantum Programs (PLQP) is a logic for describing probabilities of outcomes of quantum tests, effects of other quantum programs, as well as separation programs that characterize subsystems. In previous work, we have shown PLQP is decidable and expressed the correctness of a number of quantum protocols in PLQP. The aim of this presentation is to present a sound proof system for PLQP and use this system to prove the correctness of one protocol called quantum leader election.

---

Slides: pdf

---

Abstract: Following the tradition of separating syntax from semantics, we regard Quantum Propositional and First-Order Quantum Logicas formal languages for specifying tuples of projections in(finite-dimensional) Hilbert spaces, thus generalizing the 1D Boolean case.It turns out that also in 2D both the weak and the strong Quantum Satisfiability Problem is NP-complete.

For higher-dimensional spaces R^d and C^d with d > 2 fixed, on the other hand, we show the problem to be complete fora well-known (supposedly larger) algebraic complexity class.In particular precisely the real semi-algebraic sets can be described as as projections of (i.e. are stably equivalentto) solutions of quantum logic in-/equalities; and adding quantifiers makes the complexity climb up the polynomial hierarchy but does not increase expressibility (a property sometimes called model-completeness).

We then proceed to the questions of expressiveness and computational complexity/computability in finite but indefinite dimensions as a means towards the infinite dimensional case.

---

Slides: ppt

---

Abstract: Presheaf models (Cattani and Winskel 1997, 2003, etc.) provide an extension of labelled transtion systems that is useful for, among other things, modelling concurrent computation. This talk aims to extend such models further to represent stochastic dynamics such as shown by quantum systems. After reviewing what presheaf models represent and what certain operations on them mean in terms of notions such as internal and external choices, composition of systems, etc., I will show how to extend those models and ideas by combining them with ideas from other category-theoretic approaches to relational models and to stochastic processes. It turns out that my extension yields a transitional formulation of sheaf-theoretic structures that Abramsky and Brandenburger (2011) proposed to characterize non-locality and contextuality. An alternative characterization of contextuality will then be given in terms of a dynamic and probabilistic modal logic of the models I put forward.

---

Abstract: In this talk we will outline some work in progress in the area at the interface of Modal Logic and Category Theory. We will focus on presheaf categories and on the construction called the category of elements. Such construction can be applied in two distinct ways, depending on how we want to conceptualize the base category. When the objects of the base category are regarded as path objects (that is, computational path-shapes) we can follow the steps of Winskel, Nielsen and others, who investigated the characterization of the notion of bisimulation in terms of spans of open maps. In this context we are naturally inclined to introduce a ``path logic'', a logic that described how paths are interlinked.

If the objects of the base category are seen as types then it makes sense to perform a different variant of the category of elements. We can then show that, via such construction, each presheaf category is categorically equivalent to a special kind of transition systems (or rather, to the corresponding category). This prompts the quest for a logic that axiomatizes such class of transition systems.

---

Abstract: In this short talk, I am going to survey some important properties of the non-orthogonality relation between vectors in a Hilbert space. I will show that they imply that the collection of one-dimensional subspaces of the Hilbert space can be organized into a Kripke frame satisfying some special properties. Inspired by this, we obtain an interesting and helpful characterization of quantum dynamic frames.

---

Slides: pdf