Connectedness and acyclicity in string diagrams and proof nets II
Micah Blake McCurdy – 18 November 2009
Girard introduced proof nets for the multiplicative fragment of linear logic way back in the mists of time (1987); they are built up inductively from simple components, but not all "proof structures" actually represent proofs. Girard gave a recognition principle for determining these last, namely, that a certain pack of derived graphs be connected and acyclic.
Ross Street and I wrote a paper recently where we discussed labelling string diagrams in monoidal categories, and then considered "varying" the labelling along a Frobenius monoidal functor F. There are two obvious such "varyings", when they coincide, we say that the string diagram is F-invariant. A key result in the aforementioned paper is that a string diagram is F-invariant for all Frobenius monoidal functors if and only if it is connected and acyclic.
Robin Cockett pointed out some time ago taht specializing a linear functor between linearly distributive categories to the case where both categories have equal tensor and par produces a Frobenius monoial functor between monoidal categories. Seeing as linearly distributive categories are, by design, categorical models of the multiplicative fragment of linear logic, and string diagrams can be thought of as simple proof nets, it is tantalizing to think that the coincidence of the condition "connected and acyclic" is more than just a coincidence.
In the end, it is essentially a coincidence, as I will show; but the path to discover this gives generalizations of the results of M and Street which are themselves interesting.
Back