相关论文: Concurrency Theorems for Non-linear Rewriting Theo…

Sesqui-pushout (SqPO) rewriting is a variant of transformations of graph-like and other types of structures that fit into the framework of adhesive categories where deletion in unknown context may be implemented. We provide the first…

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…

We demonstrate that the most well-known approach to rewriting graphical structures, the Double-Pushout (DPO) approach, possesses a notion of sequential compositions of rules along an overlap that is associative in a natural sense. Notably,…

Double-pushout rewriting is an established categorical approach to the rule-based transformation of graphs and graph-like objects. One of its standard results is the construction of concurrent rules and the Concurrency Theorem pertaining to…

A foundational theory of compositional categorical rewriting theory is presented, based on a collection of fibration-like properties that collectively induce and intrinsically structure the large collection of lemmata used in the proofs of…

When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and…

String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and…

In this paper we adapt previous work on rewriting string diagrams using hypergraphs to the case where the underlying category has a traced comonoid structure, in which wires can be forked and the outputs of a morphism can be connected to…

Symmetric monoidal theories (SMTs) generalise algebraic theories in a way that make them suitable to express resource-sensitive systems, in which variables cannot be copied or discarded at will. In SMTs, traditional tree-like terms are…

In this paper we address the problem of proving confluence for string diagram rewriting, which was previously shown to be characterised combinatorically as double-pushout rewriting with interfaces (DPOI) on (labelled) hypergraphs. For…

Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories,…

We develop a theory of rewriting for structured cospans in order to extend compositional methods for modeling open networks. First, we introduce a category whose objects are structured cospans, and establish conditions under which it is…

A series of works has established rewriting as an essential tool in order to prove coherence properties of algebraic structures, such as MacLane's coherence theorem for monoidal categories, based on the observation that, under reasonable…

We demonstrate how category theory provides specifications that can efficiently be implemented via imperative algorithms and apply this to the field of graph rewriting. By examples, we show how this paradigm of software development makes it…

We extend the powerful Pullback-Pushout (PBPO) approach for graph rewriting with strong matching. Our approach, called PBPO+, allows more control over the embedding of the pattern in the host graph, which is important for a large class of…

We introduce an intuitive algorithmic methodology for enacting automated rewriting of string diagrams within a general double-pushout (DPO) framework, in which the sequence of rewrites is chosen in accordance with the causal structure of…

Equality saturation, a technique for program optimisation and reasoning, has gained attention due to the resurgence of equality graphs (e-graphs). E-graphs represent equivalence classes of terms under rewrite rules, enabling simultaneous…

Supervised and preference-based fine-tuning techniques have become popular for aligning large language models (LLMs) with user intent and correctness criteria. However, real-world training data often exhibits spurious correlations --…

String diagrams are pictorial representations for morphisms of symmetric monoidal categories. They constitute an intuitive and expressive graphical syntax, which has found application in a very diverse range of fields including concurrency…

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…