2015/11/05 by David Quick
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.195.23
published as EPTCS 195, 2015, pp. 307-320 · In Proceedings QPL 2015, arXiv:1511.01181
arxiv created 2015/11/05 · arxiv updated 2015/11/06
Diagrammatic reasoning using string diagrams provides an intuitive language for reasoning about morphisms in a symmetric monoidal category. To allow working with infinite families of string diagrams, !-graphs were introduced as a method to mark repeated structure inside a diagram. This led to !-graphs being implemented in the diagrammatic proof assistant Quantomatic. Having a partially automated program for rewriting diagrams has proven very useful, but being based on !-graphs, only commutative theories are allowed. An enriched abstract tensor notation, called !-tensors, has been used to formalise the notion of !-boxes in non-commutative structures. This work-in-progress paper presents a method to encode !-tensors as !-graphs with some additional structure. This will allow us to leverage the existing code from Quantomatic and quickly provide various tools for non-commutative diagrammatic reasoning.