Compositionality of Rewriting Rules with Conditions

TL;DR

An intricate interplay is uncovered between the category-theoretical concepts of conditions on rules and morphisms, the compositionality and compatibility of certain shift and transport constructions for conditions, and the property of associativity of the composition of rules.

Abstract

We extend the notion of compositional associative rewriting as recently studied in the rule algebra framework literature to the setting of rewriting rules with conditions. Our methodology is category-theoretical in nature, where the definition of rule composition operations encodes the non-deterministic sequential concurrent application of rules in Double-Pushout (DPO) and Sesqui-Pushout (SqPO) rewriting with application conditions based upon $\mathcal{M}$-adhesive categories. We uncover an intricate interplay between the category-theoretical concepts of conditions on rules and morphisms, the compositionality and compatibility of certain shift and transport constructions for conditions, and thirdly the property of associativity of the composition of rules.

Figures (3)

• Figure 1: Structure and original contributions of the paper.
• Figure 2: Illustration of the notion of associativity in a sequential composition of three rules with conditions. The squares explicitly marked with $\text{PO}$ are pushouts of the admissible matches of rules; all other squares are obtained according to the semantics of DPO rule compositions (and are thus also pushout squares). The top portion of the figure illustrates the order of composition ${\color{h1color}r_2 \stackrel{\mu_{21}}{\blacktriangleleft} r_1}$ followed by a composition with $r_3$ along the admissible match ${\color{h2color}\mu_{3(21)}}$. The bottom portion depicts the composition ${\color{h1color}r_3 \stackrel{\mu_{32}}{\blacktriangleleft} r_2}$ (with ${\color{h1color}\mu_{32}}$ computed via taking pullback as described in detail in Theorem \ref{['thm:assocAC']}), precomposed with $r_1$ along the induced match ${\color{h2color}\mu_{(32)1}}$. Conversely, one could start from providing explicitly the pair of admissible matches $({\color{h1color}\mu_{32}},{\color{h2color}\mu_{(32)1}})$ and compute from this data the pair of admissible matches $({\color{h1color}\mu_{21}},{\color{h2color}\mu_{3(21)}})$. Here, the composite rules' application conditions are indicated at the input interfaces of the composite rules. The second part of the statement of associativity of rule compositions entails that in both orders of pair-wise sequential compositions along the matches as specified, the resulting "triple composites" are isomorphic on their plain rule parts and have equivalent application conditions (up to satisfiability of admissible matches, i.e. in the sense of $\dot{\equiv}$).
• Figure :

Theorems & Definitions (55)

• Definition 1: Braatz:2010aa, Def. 2.1
• Definition 2: $\mathcal{M}$-initial object; Braatz:2010aa, Def. 2.5
• Lemma 1: Braatz:2010aa, Fact 2.6
• Definition 3: Finite objects, finitary categories, finitary restrictions; Braatz:2010aa, Def. 2.8 and Def. 4.1
• Theorem 1: Braatz:2010aa, Thm. 3.14
• Definition 4: Epi-$\mathcal{M}$-factorizations; cf. e.g. habel2009correctness, Def. 3
• Example 1
• Definition 5: $\mathcal{M}$-effective unions
• Theorem 2: bp2019-ext, Thm. 1.15
• Definition 6: compare lack2005adhesive, Lem. 4.9