Towards 3-Dimensional Rewriting Theory

Abstract

String rewriting systems have proved very useful to study monoids. In good cases, they give finite presentations of monoids, allowing computations on those and their manipulation by a computer. Even better, when the presentation is confluent and terminating, they provide one with a notion of canonical representative of the elements of the presented monoid. Polygraphs are a higher-dimensional generalization of this notion of presentation, from the setting of monoids to the much more general setting of n-categories. One of the main purposes of this article is to give a progressive introduction to the notion of higher-dimensional rewriting system provided by polygraphs, and describe its links with classical rewriting theory, string and term rewriting systems in particular. After introducing the general setting, we will be interested in proving local confluence for polygraphs presenting 2-categories and introduce a framework in which a finite 3-dimensional rewriting system admits a finite number of critical pairs.

References in corpus (8)

• Physics, Topology, Logic and Computation: A Rosetta Stone
• Spherical Categories
• Logical Relations for Monadic Types
• Termination orders for 3-dimensional rewriting
• The three dimensions of proofs
• Higher-dimensional categories with finite derivation type
• Two polygraphic presentations of Petri nets
• The Structure of First-Order Causality

Cited by in corpus (17)

• The algebra of entanglement and the geometry of composition
• Interacting Hopf Algebras: the theory of linear systems
• Knowledge Representation in Bicategories of Relations
• Autonomization of Monoidal Categories
• Globular: an online proof assistant for higher-dimensional rewriting
• Coherence for Frobenius pseudomonoids and the geometry of linear proofs
• Normalization for planar string diagrams and a quadratic equivalence algorithm
• Monads, partial evaluations, and rewriting
• Directed Homotopy in Non-Positively Curved Spaces
• Algebraic coherent confluence and higher globular Kleene algebras
• Computads for weak $\omega$-categories as an inductive type
• A Rewriting Coherence Theorem with Applications in Homotopy Type Theory
• Coherence for braided and symmetric pseudomonoids
• A Constructive Proof of Coherence for Symmetric Monoidal Categories Using Rewriting
• CaTT contexts are finite computads
• Zigzag normalisation for associative $n$-categories
• Presenting Finite Posets