Nicolas Behr: "Fundamentals of Compositional Rewriting Theory" скачать в хорошем качестве

Nicolas Behr: "Fundamentals of Compositional Rewriting Theory"

Topos Institute Colloquium, 9th of June 2022. ——— This presentation is based upon [1] (joint work with R. Harmer and J. Krivine). Categorical rewriting theory is a research field in both computer science and applied category theory, with a rich history spanning over 50 years of active developments, starting with the pioneering work of Ehrig in the 1970s. In this talk, I will present recent results [1] on a novel foundation for reasoning about rewriting theories via so-called compositional rewriting double categories (crDCs). The design principles followed in this approach are the typical "unify and conquer" strategy of applied category theory and a particular variant of the notion of compositionality. To wit, crDCs permit to formulate a wide variety of categorical rewriting semantics uniformly, whereby the horizontal category for a given semantics models the rewriting rules, while the vertical category models matchings and co-matchings of rules into objects, and where the squares model so-called direct derivations (i.e., individual rewriting steps). Even before considering compositionality, it is already noteworthy that in order for crDCs to be well-defined, strong constraints are imposed upon the horizontal and vertical categories and the squares of the crDC, which in effect suggest categories with adhesivity properties (e.g., toposses, quasi-toposses, adhesive HLR categories,...) as natural starting points for constructing crDCs. In this sense, the notion of crDCs thus permits to justify the by now standard approach for categorical rewriting theories developed over the past 20 years as being based upon categories with adhesivity properties (starting with the seminal work of Lack and Sobocinski on adhesive categories) from a clear mathematical high-level perspective. Compositionality, on the other hand, is a much deeper mathematical property that a categorical rewriting theory may carry. This property entails the existence of so-called Concurrency and Associativity Theorems. The former concerns being able to reason on two-step rewriting sequences via implementing the overall effect of the two-step rewrite via a composite rule applied in a single rewrite step, and vice versa. The Associativity Theorem then implies that the operation of forming compositions of rewriting rules is, in a certain sense, associative. Compositionality is a necessary and crucial ingredient in the stochastic mechanics and rule algebra formalism developed by Behr et al. since 2015, and which permits to provide a mathematically fully consistent and universal formalism for continuous- [2] and discrete-time Markov Chains [3] (central to applications of rewriting to bio- and organo-chemistry, social network modeling, etc.) and rule-algebraic combinatorics [4]. A central result of [1] is then that a sufficient set of conditions on a double category to model a compositional rewriting theory consists in requiring certain fibrational properties for the vertical source and target functors from squares of the double categories, i.e., that they are (residual) multi-opfibrations. I will sketch how these fibrational properties in conjunction with the other crDC axioms yield a completely uniform proof of both the Concurrency and the Associativity Theorems, and, time permitting, how a large variety of categorical rewriting semantics indeed fall under the umbrella of our novel crDC formalism. Finally, I will provide an overview of open questions and potential fruitful cross-connections of crDC theory with the TIC and broader ACT communities. [1] N. Behr, R. Harmer and J. Krivine, "Fundamentals of Compositional Rewriting Theory", arxiv.org/abs/2204.07175 [2] N. Behr, J. Krivine, J.L. Andersen, D. Merkle (2021), "Rewriting theory for the life sciences: A unifying theory of CTMC semantics", doi.org/10.1016/j.tcs.2021.07.026 [3] N. Behr, B.S. Bello, S. Ehmes, R. Heckel (2021), "Stochastic Graph Transformation For Social Network Modeling", doi.org/10.4204/EPTCS.350.3 [4] N. Behr (2021), "On Stochastic Rewriting and Combinatorics via Rule-Algebraic Methods", dx.doi.org/10.4204/EPTCS.334.2