Encoding !-tensors as !-graphs with neighbourhood orders

TL;DR

This paper proposes a method to encode !-tensors as !-graphs with additional structure, enabling non-commutative diagrammatic reasoning within existing graph-based proof tools.

Contribution

It introduces a novel encoding of !-tensors as !-graphs, extending the capabilities of diagrammatic reasoning tools to non-commutative theories.

Findings

Enables encoding of !-tensors as !-graphs with additional structure

Facilitates non-commutative diagrammatic reasoning in Quantomatic

Leverages existing code for broader diagrammatic reasoning applications

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.