Encoding !-tensors as !-graphs with neighbourhood orders
Abstract
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.
Cite
@article{arxiv.1511.01573,
title = {Encoding !-tensors as !-graphs with neighbourhood orders},
author = {David Quick},
journal= {arXiv preprint arXiv:1511.01573},
year = {2015}
}
Comments
In Proceedings QPL 2015, arXiv:1511.01181