Graphical languages, 27 April 2009

These are some remarks I put on department page on 27th April 2009, after talking (and writing) to Peter Selinger. I see he has just put a version of his survey on graphical languages on arxiv.

In recent times the use of graphical languages (or string diagrams) for proving algebraic facts in monoidal categories has become common.

In the following I may seem to be belabouring a simple point but I don't know how to be clear without repeating the matter several times. I have a mathematical suggestion at the end.

I think it is important to distinguish heuristic arguments from proofs. I have always used geometric heuristics in algebra since my thesis in 1970 where I used pasting diagrams in 2-categories.

However proofs traditionally consist of discrete arguments using axioms. I don't think one can be said to have a proof if it is not clear how to write down a discrete argument.

To be more precise: if the proof consists in saying the two finite graphs are isomorphic this is clearly checkable by a discrete steps. If however the proof consists in saying there is a continuous map - the continuous map must be explicitly described before you have a proof.

For this reason I don't believe that people actually use the theorems of Street and Joyal - they never check the conditions of the theorems.

This is not a criticism of their theorems - but I believe that people are really using other theorems, which may be easily deducible from Joyal-Street, but use no topology but only finite graphs (or variations).

My point is: I think it could be valuable to understand what people really are using.

I have a partial suggestion.

Consider a graph G. Adding freely a symmetric monoidal category structure plus a symmetric separable Frobenius algebra structure to each object of G yields the full subcategory of Cospan(FiniteGraphs/G) restricting to discrete graphs as objects. (Rosebrugh, Sabadini, Walters CT04). Then the free category on G is a certain subcategory: this seems an absurdly complicated thing to do but explains why the arrows in the free category are graphs labelled in G.

The point is that we could have considered instead of a graph G a "tensor graph" G whose domains and codomains are words in the objects, and do the same free construction. This leads to Cospan(FiniteTensorGraphs/G) which I guess contains many free monoidal constructions (not all!). For those free constructions it does contain it yields proofs that two expressions are equal which amount to checking isomorphisms of finite tensor graphs, instead of sequences of algebraic deductions.