Document Open Access Logo

Categorical Coherence from Term Rewriting Systems

Author Samuel Mimram

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.16.pdf
  • Filesize: 1.24 MB
  • 17 pages

Document Identifiers

Author Details

Samuel Mimram
  • LIX, École polytechnique, Palaiseau, France

Cite AsGet BibTex

Samuel Mimram. Categorical Coherence from Term Rewriting Systems. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.16

Abstract

The celebrated Squier theorem allows to prove coherence properties of algebraic structures, such as MacLane’s coherence theorem for monoidal categories, based on rewriting techniques. We are interested here in extending the theory and associated tools simultaneously in two directions. Firstly, we want to take in account situations where coherence is partial, in the sense that it only applies for a subset of structural morphisms (for instance, in the case of the coherence theorem for symmetric monoidal categories, we do not want to strictify the symmetry). Secondly, we are interested in structures where variables can be duplicated or erased. We develop theorems and rewriting techniques in order to achieve this, first in the setting of abstract rewriting systems, and then extend them to term rewriting systems, suitably generalized in order to take coherence in account. As an illustration of our results, we explain how to recover the coherence theorems for monoidal and symmetric monoidal categories.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • coherence
  • rewriting system
  • Lawvere theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Coherence theorem for monoidal categories. URL: https://ncatlab.org/nlab/show/coherence+theorem+for+monoidal+categories.
  2. Coherence theorem for symmetric monoidal categories. URL: https://ncatlab.org/nlab/show/coherence+theorem+for+symmetric+monoidal+categories.
  3. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1999. Google Scholar
  4. Marek A. Bednarczyk, Andrzej M. Borzyszkowski, and Wieslaw Pawlowski. Generalized congruences - Epimorphisms in Cat. Theory and Applications of Categories, 5(11):266-280, 1999. Google Scholar
  5. Tibor Beke. Categorification, term rewriting and the Knuth-Bendix procedure. Journal of Pure and Applied Algebra, 215(5):728-740, 2011. Google Scholar
  6. Marc Bezem, Jan Willem Klop, and Roel de Vrijer. Term rewriting systems. Cambridge University Press, 2003. Google Scholar
  7. Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria. Tape diagrams for rig categories with finite biproducts. Technical report, Università di Pisa, 2022. Google Scholar
  8. Albert Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical computer science, 115(1):43-62, 1993. Google Scholar
  9. Florence Clerc and Samuel Mimram. Presenting a category modulo a rewriting system. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  10. Jonathan Asher Cohen. Coherence for rewriting 2-theories. PhD thesis, Australian National University, 2008. URL: https://arxiv.org/abs/0904.0125.
  11. Benjamin Dupont and Philippe Malbos. Coherent confluence modulo relations and double groupoids. Journal of Pure and Applied Algebra, 226(10):107037, 2022. URL: https://arxiv.org/abs/1810.08184.
  12. John W. Gray. 2-algebraic theories and triples. Cahiers de Topologie et Géométrie Différentielle, 14:178-180, 1973. Google Scholar
  13. Yves Guiraud and Philippe Malbos. Coherence in monoidal track categories. Mathematical Structures in Computer Science, 22(6):931-969, 2012. Google Scholar
  14. Yves Guiraud and Philippe Malbos. Polygraphs of finite derivation type. Mathematical Structures in Computer Science, 28(2):155-201, 2018. Google Scholar
  15. Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM (JACM), 27(4):797-821, 1980. Google Scholar
  16. Niles Johnson and Donald Yau. 2-dimensional categories. Oxford University Press, USA, 2021. Google Scholar
  17. André Joyal and Ross Street. Braided tensor categories. Advances in Math, 102:20-78, 1993. Google Scholar
  18. Gregory Maxwell Kelly. On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra, 1(4):397-402, 1964. Google Scholar
  19. Nicolai Kraus and Jakob von Raumer. A rewriting coherence theorem with applications in homotopy type theory. Mathematical Structures in Computer Science, 32(7):982-1014, 2022. URL: https://arxiv.org/abs/2107.01594.
  20. Stephen Lack. A Quillen model structure for 2-categories. K-theory, 26(2):171-205, 2002. Google Scholar
  21. Yves Lafont. A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier). Journal of Pure and Applied Algebra, 98(3):229-244, 1995. Google Scholar
  22. Yves Lafont. Towards an algebraic theory of boolean circuits. Journal of Pure and Applied Algebra, 184(2-3):257-310, 2003. Google Scholar
  23. Yves Lafont, François Métayer, and Krzysztof Worytkiewicz. A folk model structure on omega-cat. Advances in Mathematics, 224(3):1183-1231, 2010. Google Scholar
  24. Miguel L. Laplaza. Coherence for distributivity. In Coherence in categories, pages 29-65. Springer, 1972. Google Scholar
  25. F. William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50(5):869-872, 1963. Google Scholar
  26. Saunders Mac Lane. Categories for the Working Mathematician, volume 5. Springer Science & Business Media, 1998. Google Scholar
  27. Saunders MacLane. Natural associativity and commutativity. Rice Institute Pamphlet-Rice University Studies, 49(4), 1963. Google Scholar
  28. Philippe Malbos and Samuel Mimram. Homological computations for term rewriting systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), volume 52, pages 27-1, 2016. Google Scholar
  29. Samuel Mimram and Pierre-Louis Curien. Coherent Presentations of Monoidal Categories. Logical Methods in Computer Science, 13, 2017. Google Scholar
  30. John Power. An abstract formulation for rewrite systems. In Category Theory and Computer Science, pages 300-312, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0018358.
  31. John Power. Enriched Lawvere theories. Theory and Applications of Categories, 6(7):83-93, 1999. Google Scholar
  32. Craig C. Squier, Friedrich Otto, and Yuji Kobayashi. A finiteness condition for rewriting systems. Theoretical Computer Science, 131(2):271-294, 1994. Google Scholar
  33. Ross Street. Limits indexed by category-valued 2-functors. Journal of Pure and Applied Algebra, 8(2):149-181, 1976. Google Scholar
  34. Ross Street. Categorical structures. Handbook of algebra, 1:529-577, 1996. Google Scholar
  35. Noson S. Yanofsky. The syntax of coherence. Cahiers de topologie et géométrie différentielle catégoriques, 41(4):255-304, 2000. Google Scholar
  36. Noson S. Yanofsky. Coherence, Homotopy and 2-Theories. K-Theory, 23(3):203-235, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact