Associated workshop: 19-22 March 2018
The spring 2018 meeting is subsumed by a larger workshop on Combining Viewpoints in Quantum Theory at the International Centre for Mathematical Sciences in Edinburgh.
Fourth meeting: Monday 20 November 2017
The fourth meeting will be held on 20 November 2017, in the School of Informatics at the University of Edinburgh, in room 4.31 in the morning, and room G.07 in the afternoon.
Programme:
- 10:00 Coffee
- 10:30 Tom Leinster (University of Edinburgh): A functorial approach to entropy
Ever since the early work of Grothendieck, it has been apparent that sometimes in life, cleaner theorems can be obtained by focusing on maps rather than objects. Shannon's pioneering work on information theory provided (among many other things) a unique characterization of the entropy of a finite probability space - that is, a theorem stating that it is the only quantity satisfying certain desirable properties. Other people proved other, similar characterizations. But a different kind of characterization theorem, arguably cleaner, can be obtained by moving the focus off probability spaces and onto maps between them. (This is joint work with John Baez and Tobias Fritz.) - 11:10 Danel Ahman (Inria Paris): Directed containers, what are they good for?
In this talk I will give an overview of a line of work we have carried out over the past couple of years on a specialisation of containers (aka polynomials), called directed containers, that characterise exactly those containers whose interpretation as polynomial endofunctors carries a comonad structure. I will begin by recalling the definition of directed containers; motivate them as models of tree-like data-structures where each position determines a sub-data-structure rooted at that position; and show how directed containers give rise to a comonad structure on the interpretation of the underlying container. After this, I will show that in addition to modelling tree-like data-structures, directed containers also serve as a specification of a dependently typed refinement of the state monad in which state is changed not by overwriting but by applying state-dependent updates instead; dually, they also give rise to a dependently typed updates-based refinement of asymmetric lenses. I will conclude by observing that in fact, a directed container is the same as a small category, which in turn helps one to better understand various constructions on them and on the comonads they denote. (Based on joint work with James Chapman and Tarmo Uustalu.) [slides]
- 11:50 Stanisłav Szawiel (University of Warsaw): Categories of physical processes
We study the mathematical foundations of physics. We reconstruct textbook quantum theory from a single symmetric monoidal functor GNS:Phys->*Mod, based on the Gelfand-Naimark-Segal construction and the notion of representability. We derive the probabilistic interpretation of quantum mechanics, including the Born rule, the Schrodinger and Heisenberg pictures, the relation between symmetries and group representations, and a theory of quantum Markov processes, including wave function collapse. Inclusion of the classical limit and deformation quantization is briefly sketched. Gauge symmetry and extended locality cannot currently be accommodated, due to conceptual difficulties discussed in an appendix. [slides]
- 12:20 Lunch (not catered)
- 13:20 Noam Zeilberger (University of Birmingham): A sequent calculus for a semi-associative law The classical Tamari order is the partial order on fully-bracketed words induced by a semi-associative law (ab)c <= a(bc). In the talk I will describe a simple proof-theoretic characterization of the Tamari order as a sequent calculus with a weakened version of Lambek's left rule for the non-commutative product. The main result is a "focusing" property (a strengthening of cut-elimination) for this sequent calculus, which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. One novel combinatorial application of this coherence theorem is a new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice. Finally, I will discuss how some of these ideas relate to a natural notion of "left representable" multicategory, considered independently in recent work of Bourke and Lack on skew monoidal categories. (Based on a paper presented at FSCD 2017.) [slides]
- 14:00 Ross Duncan (University of Strathclyde): Substitution, binding, and pattern matching in string diagrams Diagrams are widely used in science and engineering; well known examples include electronic circuit diagrams, Feynman diagrams, proof-nets, petri-nets, and countless others. All these diagrams share the same basic features because they are all presentations of monoidal categories - one of the most commonly encountered structures in mathematics. String diagrams are a formal syntax for monoidal categories which takes into account their two-dimensional nature, and are especially well suited to theories where sequential and parallel composition interact (or which feature both algebraic and coalgbraic operations). In this talk I’ll present some preliminary work towards theory of programming with string diagrams - namely I’ll look at how substitution and pattern matching can be defined on top of string diagrams. The putting both together results in a computad of diagram transformations. [slides]
- 14:40 Tea
- 15:10 Christian Korff (University of Glasgow): Bosons, Fermions, and 2D TQFTs Employing simple models from quantum mechanics we define families of 2D TQFTs where the fusion product is realised in terms of hopping algorithms of bosons and fermions on a circular lattice. We discuss their relation to known examples of 2D TQFTs before considering generalisations. There are combinatorial connections with the counting of dimer configurations and cylindric reverse plane partitions.
- 15:50 Bob Coecke (University of Oxford): From quantum foundations to cognition and the class room via pictures For well over a decade, we developed an entirely pictorial presentation of quantum theory [*]. An important recent development post [*] concerns completeness of the language, i.e. diagrammatic calculus can reproduce all equationa that are derivable in Hilbert space. At the present, experiments are being setup aimed at establishing the age at which children could effectively learn quantum theory in this manner. Meanwhile, the pictorial language has also been successful in the study of natural language, and very recently we have started to apply it to model cognition. We present the key ingredients of the pictorial language language as well as their interpretation across disciplines. [*] B. Coecke & A. Kissinger (2017) Picturing Quantum Processes. A first course on quantum theory and diagrammatic reasoning. Cambridge University Press. [slides]
- 16:30 Quanlong Wang (University of Oxford): Construction of protocols for quantum encryption, key distribution and bit commitment via categorical quantum mechanics
Here we apply categorical quantum mechanics (CQM) to the design of quantum cryptographic protocols. We first develop a quantum encryption scheme by making using of phase shift over complementary observables. We then construct a quantum three-pass protocol for key distribution, based on our quantum encryption scheme. We show that our encryption scheme and protocol for key distribution are informationally secure. We further study and propose a quantum bit commitment (QBC) protocol inspired by the framework of CQM. We show that our QBC protocol is more efficient and secure than most existing cheat-sensitive QBC protocols. We prove the correctness of all our scheme/protocols by the graphical calculus of CQM. Finally, we run experiments on the IBM quantum computer to demonstrate that our protocols are implementable by the current technology. [slides]
- 17:00 Pub
Registration is free, but for catering purposes please email the local organiser Chris Heunen as soon as possible if you plan to attend.
Third meeting: Wednesday 5 April 2017
The third meeting was held on 5 April 2017, in the Department of Computer and Information Sciences at the University of Strathclyde, in room 1415 of Livingston Tower.
Programme:
- 10:00: Coffee
- 10:30: Kevin Dunne (University of Strathclyde): Infinite-Dimensional Categorical Quantum Mechanics, Spectra, and Contextuality
There have been several projects reformulating some aspect of quantum theory in the language of category theory, for example: the monoidal approach to quantum theory, which encodes aspects of quantum theory as algebras internal to some symmetric monoidal category (e.g. Frobenius, Hopf, or H*-algebras); the topos approach of Butterfield, Isham and Doering, which embeds traditional quantum theory into a the framework of topos theory; and an approach to quantum logic of Heunen and Jacobs based on the semilattice structures associated with dagger-kernel categories.
These three approaches are independent of one another, however we show an interaction between them. The combined approach embeds the monoidal approach into a topos framework, and with the addition of dagger-kernels we can derive structure theorems for Frobenius algebras and H*-algebras. Analogous to studying groups by considering their linear representations, we give a canonical representation theory for the kinds of internal algebras typically studied in the monoidal approach to quantum theory. We can then use these structure theorems to address the question of whether or not a category exhibits contextuality, in particular we obtain a proof that the category of sets and relations is non-contextual. [slides] [video] - 11:10: Chris Heunen (University of Edinburgh): The category of Hilbert modules
Categorical quantum mechanics abstracts away from Hilbert spaces to see how much of quantum theory can be given a conceptual categorical basis. Nevertheless, the main examples remain based on Hilbert spaces or sets and relations. In particular, the scalars are usually thought of as numbers. I will discuss the category of Hilbert modules, where the scalars hide the structure an underlying space(time). The objects may be regarded as state spaces that vary continuously over a base space(time). Hence the category may be regarded as capturing a naive quantum field theory rather than quantum mechanics. I will analyse the Frobenius structures in this category and give nontrivial infinite-dimensional examples. I will also discuss localisation: open subsets of the base space correspond to idempotent subobjects of the tensor unit. Finally, I will discuss work in progress about applying these techniques to categorify relativistic quantum information theory. [slides] [video]
- 11:50: Fabio Zanasi (University College London): A new foundation for string diagram rewriting: adequacy, confluence, commutativity
String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. In this work we give a sound and complete interpretation for this form of rewriting in terms of double pushout (DPO) rewriting of hypergraphs, subject to a convexity condition. Non-convex rewriting in this domain is also interesting, as syntactically it corresponds to rewriting modulo a chosen separable Frobenius structure. Time permitting, two further results strengthening this approach will be shown. The first is that, contrary to arbitrary hypergraph rewriting, with our setup confluence becomes decidable for terminating rewriting systems. The second is a sound and complete interpretation of commutative operators as additional Frobenius structures, which addresses the problem of non-termination of commutativity as a rewrite rule. [slides] [video]
- 12:30: Lunch
- 14:00: Aleks Kissinger (Radboud University): A categorical semantics for causal structure
I'll present a categorical construction for modelling both definite and indefinite causal structures within a general class of process theories that include classical probability theory and quantum theory. Unlike prior constructions within categorical quantum mechanics, the objects of this theory encode finegrained causal relationships between subsystems and give a new method for expressing and deriving consequences for a broad class of causal structures. I'll give several examples, including non-signalling processes, quantum n-combs, and OCB process matrices and show how the operational behaviour of such processes can be derived from the categorical structure. [slides] [video]
- 14:40: Stefano Gogioso (University of Oxford): Infinite-dimensional Categorical Quantum Mechanics
I will present some recent developments in the non-standard framework for infinite-dimensional categorical quantum mechanics. I will start by introducing the category Star Hilb, which is dagger compact and comes with unital dagger Frobenius algebras. I will provide explicit constructions for the Hilbert spaces of wavefunctions in boxes with periodic boundary conditions, wavefunctions on lattices, and wavefunctions in real space. Time permitting, I will also sketch a couple of constructions of interest in quantum field theory. [slides] [video]
- 15:20: Tea
- 15:40: Peter Hines (University of York): Diagrams and Coherence Theorems in Cryptography and Cryptanalysis
This talk intends to demonstrate that categorical diagrams are a simple and convenient way of visualising and reasoning about cryptographic protocols. We illustrate this with various examples of both popular and obscure protocols, to demonstrate how the flow of information among the participants may be modelled. We also provide evidence for the claim that there are deeper connections between category theory, complexity, and cryptography than simply modelling information flow.
The talk is very much aimed at category theorists who are interested in how their field may be applied to cryptography, rather than vice versa. No prior knowledge of cryptography is required, but some category-theoretic background will be assumed! [slides] [video] - 16:20: Clemens Kupke (University of Strathclyde) Games for topological fixpoint logics Topological fixpoint logics are logics that are interpreted over topological models and where the fixpoint operators are defined with respect to these topological interpretations. In my talk I will discuss a variant of these logics for relational structures based on Stone spaces, where the fixpoint operators are interpreted via clopen sets. I will present a game-theoretic semantics for this logic. The adequacy and bisimulation-invariance of this semantics will be the main technical results of my talk.
The motivation for this work is two-fold: i) studying topological models of modal fixpoint logics might shed new light on completeness proofs for these logics and ii) restricting the interpretation of formulas to so-called admissible subsets of the model adjusts the expressiveness of the logic to capture natural topological properties of the model (e.g. reachability-in-the-limit as opposed to standard reachability). [slides] [video] - 17:00: Pub
Registration is free, but for catering purposes please email the local organiser Ross Duncan as soon as possible if you plan to attend.
You might also be interested in the workshop on Algebra and Coalgebra meet Proof Theory held at the University of Strathclyde on April 10-12.
Second meeting: Wednesday 30 November 2016
The second meeting was held on 30 November 2016, in the Department of Computer and Information Sciences at the University of Strathclyde, in room 1415 of Livingston Tower.
Programme:
- 10:00: Coffee
- 10:30: Ulrich Kraehmer (University of Glasgow): What is a quantum symmetry?
Since the 1980s, algebraists studied quantum groups (Hopf algebras) as generalised symmetries, and they extended various concepts and results from group theory to quantum groups. After giving a small survey of this story, I will explain a paper with Angela Tabiri in which we show that planar curves have way more quantum symmetries than classical ones, and also more than we expected. [slides] [video]
- 11:15: Kevin Dunne (University of Strathclyde): Endomorphism semialgebras in categorical quantum mechanics
The category Rel of sets and relations has been studied extensively from the perspective of the monoidal approach to quantum theory. Here we take a look at Rel from the perspective of the topos approach to quantum theory. To do this we must generalise aspects of the topos approach to quantum theory, in particular we generalise C*-algebras and their Gelfand spectrum, which we do using the language of semialgebras. We will then compare this perspective of Rel to that of the monoidal approach to quantum theory, and see a surprisingly similar picture emerge to that of the category of finite dimensional Hilbert spaces. [slides] [video]
- 12:00: Martti Karvonen (University of Edinburgh): Dagger categories: monads and limits
A dagger category is a category equipped with a dagger: a contravariant involutive identity-on-objects endofunctor. Such categories are used to model quantum computing and reversible computing, amongst others. The philosophy when working with dagger categories is that all structure in sight should cooperate with the dagger. This causes dagger category theory to differ in many ways from ordinary category theory. Standard theorems have dagger analogues once one figures out what "cooperation with the dagger" means for each concept, but often this is not just an application of formal 2-categorical machinery or a passage to (co)free dagger categories. We will discuss two instances.
First, as soon as a monad on a dagger category satisfies the Frobenius law, everything works as it should. Dagger adjunctions give riseto such monads. Conversely, such monads factor as dagger adjunctions in two canonical ways; however, the Eilenberg-Moore category needs to be adapted t o inherit the dagger.
Second, limits in dagger categories should be unique up to an unique unitary, that is, an isomorphism whose inverse is its dagger. We rework an initial attempt to a more elegant and general theory. It works well when the diagram has a dagger; however, the formulation of limits using adjunctions needs to be adapted. We will discuss work on defining dagger limits of general diagrams.
Finally, we will discuss formally how dagger categories, while perhaps slightly evil, are not all that bad. [slides] [video] - 12:45: Lunch
- 14:15: Tarmo Uustalu (Tallinn University of Technology):
Grading monads, comonads and distributive laws
We are accustomed to using strong monads to organize effectful computations in programming language semantics and monoidal comonads in a similar vein to organize coeffectful computations. I will show how a quantitative aspect can be added by grading, leading to mathematization of the old idea of effect systems from program analysis. I will first introduce graded (strong) monads, outlining both their theory and programming language applications, and will then discuss graded monads of monoids, graded distributive laws of a monad over a monad, graded (monoidal) comonads and distributive laws of a comonad over a monad.
This is based on recent works by Soichiro Fujii, Shin-ya Katsumata, Paul-André Melliès, Flavien Breuvart, Marco Gaboardi, Dominic Orchard and myself. [slides] [video] - 15:00: Dan Marsden (University of Oxford): Custom hypergraph categories via generalized relations
Compact closed and hypergraph categories have become standard settings for work in categorical quantum mechanics, linguistics and general process theories. More recently, our group in Oxford has been looking at further applications in areas such as cognition. With each new application area, there is a need to identify a suitable category modelling thppe phenomena under consideration. In this talk we will describe a framework derived from generalized notions of relations, in which we can construct hypergraph categories which can capture features such as convexity, proof relevance, metrics and semantics varying with time or context. The framework is parameterized along 4 natural axes of variation, allowing users to flexibly configure hypergraph categories to their application needs. [slides] [video]
- 15:45: Tom Avery (University of Edinburgh): Notions of algebraic theory
Intuitively, an algebraic theory is a kind of mathematical structure defined by some operations with various arities, that satisfy certain equations. There are lots of categorical ways of making this precise at various levels of generality, including monads, Lawvere theories, PROPs, monoids, and monads with arities. I will describe a notion of algebraic theory that specialises to each of these, and discuss some results that can be proved even at this very high level of generality. [video]
- 16:30: Tea and discussion
Registration is free, but for catering purposes please email the local organiser Ross Duncan as soon as possible if you plan to attend.
You might also be interested in the workshop on coalgebra, Horn clause logic programming and types held at the University of Edinburgh on November 28 and 29.
First meeting: Thursday 14 April 2016
The first meeting was held on 14 April 2016, in the School of Informatics at the University of Edinburgh, room G.07.
Programme:
- 10:30: Coffee
- 11:00: Stefano Gogioso (University of Oxford): Fully graphical treatment of the Hidden Subgroup Problem
The Hidden Subgroup Problem (HSP) encompasses several more specific problems of interest in quantum computation. Integer factorisation and the discrete logarithm are both special cases of the abelian HSP, while the graph isomorphism problem is a special case of the (yet-to-be-solved) non-abelian HSP. Today, we present the first fully-graphical treatment of the quantum algorithm for the abelian HSP. We highlight the key role played by strongly complementary observables in its formulation, and we investigate the extent to which they could be used to tackle the non-abelian HSP. [video]
- 11:40: Sean Tull (University of Oxford): Operational physics, logic and categories
Recent years have seen several reconstructions of quantum theory from among more general operational theories of physics, defined in terms of systems and probabilistic experiments one may perform upon them. A major example is the framework of 'operational-probabilistic theories' due to Chiribella, D'Ariano and Perinotti. I will introduce a close variant of these operational theories and show how they can be treated in an entirely categorical way, using the new notion of an operational category. Our approach comes from effectus theory, an area of categorical logic due to Jacobs, which we offer a new operational interpretation. This perspective also establishes interesting connections between the programmes of general probabilistic theories and categorical quantum mechanics. [slides] [video]
- 12:20: Sander Uijlen (Radboud University): Indefinite causal structures using diagrammatic methods
If we abandon the idea of a fixed causal structure and use local quantum mechanics, we can obtain probability distributions which are incompatible with even convex mixtures of causal structures. In this talk we take a look at some preliminary results of an investigation of these indefinite causal structures using diagrammatic methods. [slides] [video]
- 13:00: Lunch
- 14:00: Nick Behr (University of Edinburgh): Graph rewriting and combinatorial Hopf algebra
A novel formulation of graph rewriting will be presented, the so-called rule algebraic formalism. Its mathematical foundation lies in the concept of a certain combinatorial Hopf algebra, namely the algebra of compositions of rule diagrams. The algebras of graph rewriting in its four different variants may be obtained in the form of reductions of the rule diagram algebra. Remarkably, the definition and study of the algebras of graph rewriting appear to be entirely new concepts, and yield powerful new approaches for both theory and applications. The focus of this talk will be the interplay between mathematical structure and some of these new approaches. The work presented is joint work with V. Danos and I. Garnier (LFCS/ENS Paris) and (in an earlier phase) T. Heindel (University of Copenhagen). [slides] [video]
- 14:40: Mark Lawson (Heriot-Watt University): Inverse semigroups and étale groupoids
- 15:20: Tea
- 15:40: Bob Atkey (University of Strathclyde): From parametricity to conservation laws, via Noether's theorem
Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds' theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields "free" theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy is by Noether's theorem a consequence of a system's invariance under time-shifting.
I will show a way to link Reynolds' relational parametricity with Noether's theorem. I'll discuss an extension of System Fω with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. I'll show, by constructing a relationally parametric model, that relational parametricity is enough to satisfy the hypotheses of Noether's theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system. [slides] [video] - 16:20: Christian Saemann (Heriot-Watt University): Categorical description of gauge theory
I will describe a very general approach to higher gauge theory and higher gauged sigma models that allows for arbitrary higher groupoids as spacetimes, target spaces and higher gauge groups. Various applications to physics and in particularly string theory will be pointed out. At the end, I will list some of the important open problems in this context. [slides] [video]
- 17:00: Gwendolyn Barnes (Heriot-Watt University): A category theoretic framework for noncommutative and nonassociative geometry
Observations from flux compactifications of closed string theory suggest that a theory of gravity at quantum scales may be not only noncommutative but also nonassociative. Having an abstract understanding of geometry is one approach to help us to describe a noncommutative and nonassociative theory of gravity. In work together with Alexander Schenkel and Richard J. Szabo we have appealed to the tools of category theory to better understand the mathematical structures underlying noncommutative and nonassociative deformations of spacetime geometry. [slides] [video]
- 17:40: Pub
Registration is free, but for catering purposes please email the local organiser Chris Heunen as soon as possible if you plan to attend.
You might also be interested in two events earlier in the week: WadlerFest 2016 on Monday and Tuesday, and LFCS30 on Tuesday and Wednesday.
Sponsored by 