Subsumptions of Algebraic Rewrite Rules

Thierry Boy de la Tour
(Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG)

What does it mean for an algebraic rewrite rule to subsume another rule (that may then be called a subrule)? We view subsumptions as rule morphisms such that the simultaneous application of a rule and a subrule (i.e. the application of a subsumption morphism) yields the same result as a single application of the subsuming rule. Simultaneous applications of categories of rules are obtained by Global Coherent Transformations and illustrated on graphs in the DPO approach. Other approaches are possible since these transformations are formulated in an abstract Rewriting Environment, and such environments exist for various approaches to Algebraic Rewriting, including DPO, SqPO and PBPO.

In Sam Staton and Christina Vasilakopoulou: Proceedings of the Sixth International Conference on Applied Category Theory 2023 (ACT 2023), University of Maryland, 31 July - 4 August 2023, Electronic Proceedings in Theoretical Computer Science 397, pp. 20–38.
Published: 14th December 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.397.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org