Taking advantage of a recently discovered associativity property of rule compositions, we extend the classical concurrency theory for rewriting systems over adhesive categories. We introduce the notion of tracelets, which are defined as minimal derivation traces that universally encode sequential compositions of rewriting rules. Tracelets are compositional, capture the causality of equivalence classes of traditional derivation traces, and intrinsically suggest a clean mathematical framework for the definition of various notions of abstractions of traces. We illustrate these features by introducing a first prototype for a framework of tracelet analysis, which as a key application permits to formulate a first-of-its-kind algorithm for the static generation of minimal derivation traces with prescribed terminal events.
In: John Baez and Bob Coecke: Proceedings Applied Category Theory 2019 (ACT 2019), University of Oxford, UK, 15-19 July 2019, Electronic Proceedings in Theoretical Computer Science 323, pp. 44-71.
Thanks to the Statebox team, there is a video recording available of my talk (uploaded to youtube by Jelle Herold; due to some technical difficulties with a drop of recording in the middle, there are two parts to the recording):
Schematic overview of the tracelet and tracelet analysis framework.
Three rules sequentially composed (from right to left): input and output interfaces are drawn explicitly, while the context graphs $K_j$ are implicitly encoded as subgraphs of $O_j$ and $I_j$ joined by dotted lines (for $j=1,2,3$). The structure of the matches of the rules is indicated via lines connecting elements of outputs to elements of inputs of rules.
Explicit demonstration of the associativity property of the rule composition operation: the top half of the diagram encodes a composition of the shape $r_3\triangleleft (r_2 \triangleleft r_3)$, while the bottom half encodes $(r_3 \triangleleft r_2)\triangleleft r_1$, with both operations for the overlaps depicted leading to the same minimal trace (up to isomorphisms). The tracelet of length $3$ equivalently encoded by both halves of the diagram is obtained by composition of squares.
