Abstract:
A research programme is set out for developing the use of high-level methods for quantum computation and information, based on the categorical formulation of quantum mechanics introduced by the author and Bob Coecke.

Abstract:
We use a simple relational framework to develop the key notions and results on hidden variables and non-locality. The extensive literature on these topics in the foundations of quantum mechanics is couched in terms of probabilistic models, and properties such as locality and no-signalling are formulated probabilistically. We show that to a remarkable extent, the main structure of the theory, through the major No-Go theorems and beyond, survives intact under the replacement of probability distributions by mere relations.

Abstract:
Recently, the author and Bob Coecke have introduced a categorical formulation of Quantum Mechanics. In the present paper, we shall use it to open up a novel perspective on No-Cloning. What we shall find, quite unexpectedly, is a link to some fundamental issues in logic, computation, and the foundations of mathematics. A striking feature of our results is that they are visibly in the same genre as a well-known result by Joyal in categorical logic showing that a `Boolean cartesian closed category' trivializes, which provides a major road-block to the computational interpretation of classical logic. In fact, they strengthen Joyal's result, insofar as the assumption of a full categorical product (both diagonals and projections) in the presence of a classical duality is weakened. This shows a heretofore unsuspected connection between limitative results in proof theory and No-Go theorems in quantum mechanics.

Abstract:
We study structures which have arisen in recent work by the present author and Bob Coecke on a categorical axiomatics for Quantum Mechanics; in particular, the notion of strongly compact closed category. We explain how these structures support a notion of scalar which allows quantitative aspects of physical theory to be expressed, and how the notion of strong compact closure emerges as a significant refinement of the more classical notion of compact closed category. We then proceed to an extended discussion of free constructions for a sequence of progressively more complex kinds of structured category, culminating in the strongly compact closed case. The simple geometric and combinatorial ideas underlying these constructions are emphasized. We also discuss variations where a prescribed monoid of scalars can be "glued in" to the free construction.

Abstract:
We pursue a model-oriented rather than axiomatic approach to the foundations of Quantum Mechanics, with the idea that new models can often suggest new axioms. This approach has often been fruitful in Logic and Theoretical Computer Science. Rather than seeking to construct a simplified toy model, we aim for a `big toy model', in which both quantum and classical systems can be faithfully represented - as well as, possibly, more exotic kinds of systems. To this end, we show how Chu spaces can be used to represent physical systems of various kinds. In particular, we show how quantum systems can be represented as Chu spaces over the unit interval in such a way that the Chu morphisms correspond exactly to the physically meaningful symmetries of the systems - the unitaries and antiunitaries. In this way we obtain a full and faithful functor from the groupoid of Hilbert spaces and their symmetries to Chu spaces. We also consider whether it is possible to use a finite value set rather than the unit interval; we show that three values suffice, while the two standard possibilistic reductions to two values both fail to preserve fullness.

Abstract:
We revisit our earlier work on the representation of quantum systems as Chu spaces, and investigate the use of coalgebra as an alternative framework. On the one hand, coalgebras allow the dynamics of repeated measurement to be captured, and provide mathematical tools such as final coalgebras, bisimulation and coalgebraic logic. However, the standard coalgebraic framework does not accommodate contravariance, and is too rigid to allow physical symmetries to be represented. We introduce a fibrational structure on coalgebras in which contravariance is represented by indexing. We use this structure to give a universal semantics for quantum systems based on a final coalgebra construction. We characterize equality in this semantics as projective equivalence. We also define an analogous indexed structure for Chu spaces, and use this to obtain a novel categorical description of the category of Chu spaces. We use the indexed structures of Chu spaces and coalgebras over a common base to define a truncation functor from coalgebras to Chu spaces. This truncation functor is used to lift the full and faithful representation of the groupoid of physical symmetries on Hilbert spaces into Chu spaces, obtained in our previous work, to the coalgebraic semantics.

Abstract:
Our aim in this paper is to trace some of the surprising and beautiful connections which are beginning to emerge between a number of apparently disparate topics: Knot Theory, Categorical Quantum Mechanics, and Logic and Computation. We shall focus in particular on the following two topics: - The Temperley-Lieb algebra has always hitherto been presented as a quotient of some sort: either algebraically by generators and relations as in Jones' original presentation, or as a diagram algebra modulo planar isotopy as in Kauffman's presentation. We shall use tools from Geometry of Interaction, a dynamical interpretation of proofs under Cut Elimination developed as an off-shoot of Linear Logic, to give a direct description of the Temperley-Lieb category -- a "fully abstract presentation", in Computer Science terminology. This also brings something new to the Geometry of Interaction, since we are led to develop a planar version of it, and to verify that the interpretation of Cut-Elimination (the "Execution Formula", or "composition by feedback") preserves planarity. - We shall also show how the Temperley-Lieb algebra provides a natural setting in which computation can be performed diagrammatically as geometric simplification -- "yanking lines straight". We shall introduce a "planar lambda-calculus" for this purpose, and show how it can be interpreted in the Temperley-Lieb category.

Abstract:
We give multiple descriptions of a topological universe of finitary sets, which can be seen as a natural limit completion of the hereditarily finite sets. This universe is characterized as a metric completion of the hereditarily finite sets; as a Stone space arising as the solution of a functorial fixed-point equation involving the Vietoris construction; as the Stone dual of the free modal algebra; and as the subspace of maximal elements of a domain equation involving the Plotkin (or convex) powerdomain. These results illustrate the methods developed in the author's 'Domain theory in logical form', and related literature, and have been taken up in recent work on topological coalgebras. The set-theoretic universe of finitary sets also supports an interesting form of set theory. It contains non-well founded sets and a universal set; and is closed under positive versions of the usual axioms of set theory.

Abstract:
Connections between the sequentiality/concurrency distinction and the semantics of proofs are investigated, with particular reference to games and Linear Logic.

Abstract:
Reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. Most foundational work on reversible computing to date has focussed on simulations of low-level machine models. By contrast, we develop a more structural approach. We show how high-level functional programs can be mapped compositionally (i.e. in a syntax-directed fashion) into a simple kind of automata which are immediately seen to be reversible. The size of the automaton is linear in the size of the functional term. In mathematical terms, we are building a concrete model of functional computation. This construction stems directly from ideas arising in Geometry of Interaction and Linear Logic---but can be understood without any knowledge of these topics. In fact, it serves as an excellent introduction to them. At the same time, an interesting logical delineation between reversible and irreversible forms of computation emerges from our analysis.