Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Critical Pair Enumeration Algorithm for String Diagram Rewriting

Anna Matsui, Innocent Obi, Guillaume Sabbagh, Leo Torres, Diana Kessler, Juan F. Meleiro, Koko Muroya

TL;DR

This work aims at automation of critical pair analysis for string diagram rewriting, and develops an algorithm that implements the core part of critical pair analysis, and proves correctness and exhaustiveness of the algorithm, for string diagrams in symmetric monoidal categories without a Frobenius structure.

Abstract

Critical pair analysis provides a convenient and computable criterion of confluence, which is a fundamental property in rewriting theory, for a wide variety of rewriting systems. Bonchi et al. showed validity of critical pair analysis for rewriting on string diagrams in symmetric monoidal categories. This work aims at automation of critical pair analysis for string diagram rewriting, and develops an algorithm that implements the core part of critical pair analysis. The algorithm enumerates all critical pairs of a given left-connected string diagram rewriting system, and it can be realised by concrete manipulation of hypergraphs. We prove correctness and exhaustiveness of the algorithm, for string diagrams in symmetric monoidal categories without a Frobenius structure.

A Critical Pair Enumeration Algorithm for String Diagram Rewriting

TL;DR

This work aims at automation of critical pair analysis for string diagram rewriting, and develops an algorithm that implements the core part of critical pair analysis, and proves correctness and exhaustiveness of the algorithm, for string diagrams in symmetric monoidal categories without a Frobenius structure.

Abstract

Critical pair analysis provides a convenient and computable criterion of confluence, which is a fundamental property in rewriting theory, for a wide variety of rewriting systems. Bonchi et al. showed validity of critical pair analysis for rewriting on string diagrams in symmetric monoidal categories. This work aims at automation of critical pair analysis for string diagram rewriting, and develops an algorithm that implements the core part of critical pair analysis. The algorithm enumerates all critical pairs of a given left-connected string diagram rewriting system, and it can be realised by concrete manipulation of hypergraphs. We prove correctness and exhaustiveness of the algorithm, for string diagrams in symmetric monoidal categories without a Frobenius structure.
Paper Structure (13 sections, 13 theorems, 3 equations, 4 algorithms)

This paper contains 13 sections, 13 theorems, 3 equations, 4 algorithms.

Table of Contents

  1. Introduction
  2. Rewriting Theory and Critical Pair Analysis
  3. String Diagram Rewriting
  4. Contributions
  5. Organisation.
  6. Related work.
  7. Critical Pairs for String Diagram Rewriting
  8. Hypergraphs with Interface
  9. Convex DPOI Rewriting
  10. Critical Pairs
  11. A Critical Pair Enumeration Algorithm
  12. An Optimisation
  13. Conclusion and Future Work

Key Result

Proposition 2.10

In left-connected rewrite systems, the boundary complement condition is always met. In left-connected rewrite systems, a mono match is always convex.

Theorems & Definitions (34)

  • Definition 2.1: Hypergraphs
  • Definition 2.2: Hypergraph morphisms
  • Definition 2.3: $\Sigma$-hypergraph with interfaces
  • Definition 2.4: Paths
  • Definition 2.5: Monogamous acyclicity
  • Definition 2.6: Strong connectivity
  • Definition 2.7: Convex matches
  • Definition 2.8: Boundary complement
  • Definition 2.9: Convex rewriting
  • Proposition 2.10
  • ...and 24 more