Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Adhesive category theory for graph rewriting in Rocq

Samuel Arsac, Russ Harmer, Damien Pous

TL;DR

This work designs a Rocq library about adhesive categories, using Hierarchy Builder, and formalizes two central theorems of categorical graph rewriting theory: the Church-Rosser theorem and the concurrency theorem.

Abstract

We design a Rocq library about adhesive categories, using Hierarchy Builder (HB). It is built around two hierarchies. The first is for categories, with usual categories at the bottom and adhesive categories at the top, with weaker variants of adhesive categories in between. The second is for morphisms (notably isomorphisms, monomorphisms and regular monomorphisms). Each level of these hierarchies is equipped with several interfaces to define instances. We cover basic categorical concepts such as pullbacks and equalizers, as well as results specific to adhesive categories. Using this library, we formalize two central theorems of categorical graph rewriting theory: the Church-Rosser theorem and the concurrency theorem. We provide several instances, including the category of types, the category of finite types, the category of simple graphs and categories of presheaves. We detail the implementation choices we made and report on the usage of HB for this formalization work.

Adhesive category theory for graph rewriting in Rocq

TL;DR

This work designs a Rocq library about adhesive categories, using Hierarchy Builder, and formalizes two central theorems of categorical graph rewriting theory: the Church-Rosser theorem and the concurrency theorem.

Abstract

We design a Rocq library about adhesive categories, using Hierarchy Builder (HB). It is built around two hierarchies. The first is for categories, with usual categories at the bottom and adhesive categories at the top, with weaker variants of adhesive categories in between. The second is for morphisms (notably isomorphisms, monomorphisms and regular monomorphisms). Each level of these hierarchies is equipped with several interfaces to define instances. We cover basic categorical concepts such as pullbacks and equalizers, as well as results specific to adhesive categories. Using this library, we formalize two central theorems of categorical graph rewriting theory: the Church-Rosser theorem and the concurrency theorem. We provide several instances, including the category of types, the category of finite types, the category of simple graphs and categories of presheaves. We detail the implementation choices we made and report on the usage of HB for this formalization work.

Paper Structure

This paper contains 33 sections, 2 theorems, 5 figures.

Table of Contents

  1. Introduction
  2. General Category Theory
  3. Equality on Morphisms
  4. The Hierarchies of Categories and Morphisms
  5. Notations
  6. Bundling
  7. A Concrete Example: Regular Monos
  8. Duality
  9. Adhesive Category Theory
  10. Van Kampen Squares and Adhesive Morphisms
  11. Subobjects
  12. The Hierarchy of Adhesive Categories
  13. Rm-quasiadhesive Categories
  14. Rm-adhesive Categories
  15. Adhesive Categories
  16. ...and 18 more sections

Key Result

theorem 2

In a category $\mathbf{C}$ with all pullbacks, the following are equivalent:

Figures (5)

  • Figure 1: The two hierarchies in the library. An arrow from a structure A to a structure B means that every instance of A is also an instance of B, i.e., A inherits from B.
  • Figure 2: The extended hierarchy of morphisms: with non-forgetful inheritance (top) or with extended isomorphisms (bottom).
  • Figure 3: Extended hierarchy of categories.
  • Figure 4: An example of a production with simple graphs. The edge is deleted, and a new vertex with an edge is added
  • Figure 5: $\mathbf{SGraphs}$ is not rm-adhesive.

Theorems & Definitions (8)

  • Remark 1
  • definition 1: Van Kampen square lackAdhesiveQuasiadhesiveCategories2005
  • definition 2: Adhesive morphisms garnerAxiomsAdhesiveQuasiadhesive2012
  • definition 3: Rm-quasiadhesive category garnerAxiomsAdhesiveQuasiadhesive2012
  • definition 4: Rm-adhesive category garnerAxiomsAdhesiveQuasiadhesive2012, lackAdhesiveQuasiadhesiveCategories2005
  • theorem 2: garnerAxiomsAdhesiveQuasiadhesive2012
  • definition 5: Adhesive category garnerAxiomsAdhesiveQuasiadhesive2012
  • theorem 3: garnerAxiomsAdhesiveQuasiadhesive2012 and lackAdhesiveQuasiadhesiveCategories2005