Thinking through diagrams
The theory of geometry developed by the Greek mathematician Euclid about 2300 years ago was notable for two original features: First, it was what we now call axiomatic. Euclid started with some explicit assumptions (called axioms) and rules of inference and then he developed the logical consequences of these assumptions and inference rules. It wasn’t until the 1890s, however, that other mathematicians (initially Mario Pieri and David Hilbert) took this idea and ran with it, presenting formal axiomatic treatments of geometry. Bertrand Russell and Alfred North Whitehead famously developed an axiomatic treatment for mathematics in general, in their book Principia Mathematica (published 1910-1913).
Second, the rules of inference used by Euclid were essentially diagrammatic — the drawings of circles, triangles and other shapes in the Mediterranean sand were not merely illustrations of mathematical reasoning, but were the means by which this reasoning occurred. For most of the time since Euclid, mathematics has been done via text and symbols rather than by diagrams. Only with the rise of Category Theory in the last 60 years have we seen another branch of pure mathematics where reasoning is done explicitly through diagrams, in this case, what are called commutative diagrams.
Why is this relevant to computer science? Well, computers can reason equally well with symbols as with diagrams, since both are converted (ultimately) to binary digits. But our western text-oriented culture has mostly favoured the manipulation of textual symbols rather than the manipulation of diagrams or images. Only in recent years have researchers in computer science, pure mathematics, and theoretical physics begun looking systematically at diagrammatic representations and reasoning.
This post is to introduce our first Informatics Department Colloquium for the 2012 academic year. This Colloquium will be given on Wednesday 31 October 2012 at 17:00 by Dr Aleks Kissinger of Oxford University on the topic of “String Graph Rewriting and Free Monoidal Categories”. The location for this talk will be Seminar Room K2.31, Second Floor of the King’s Building at the Strand Campus. Meanwhile, the abstract for Dr Kissinger’s talk is here:
String diagrams are a powerful tool for reasoning about physical processes, logic circuits, tensor networks, and many other compositional structures. In 1991, Joyal and Street provided a topological formalisation of string diagrams and used them to construct free monoidal categories.
In this talk, I will show how string diagrams can be represented in a manner amenable to automation using special kinds of typed graphs called string graphs. I’ll then demonstrate the construction of free traced symmetric monoidal categories as well as “diagrammatically presented” categories, i.e., the most general categories admitting a given set of graph rewrite rules. If there’s time, I will also talk about extensions to the diagrammatic language to admit graph patterns, and our implementation in Quantomatic.”