Semantics-Preserving DPO-Based Term Graph Rewriting

黏合范畴中的规则代数

Rule Algebras for Adhesive Categories

本文证明双推重写在黏合范畴中沿重叠的规则顺序组合具有自然结合性，并定义了规则代数，在具有初始对象时得到单位代数，为随机DPO重写系统中统计矩的计算提供了规范表示。

Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems

In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is a sound structure-preserving transformation for weakly-left-linear deterministic conditional term rewriting systems. More precisely, we show that every weakly-left-linear deterministic conditional term rewriting system can be converted to an equivalent weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting system and prove that the SR transformation is sound for weakly-left-linear and ultra-weakly-left-linear deterministic condition…

Graph Rewriting and Relabeling with PBPO+

We extend the powerful Pullback-Pushout (PBPO) approach for graph rewriting with strong matching. Our approach, called \pbpostrong, exerts more control over the embedding of the pattern in the host graph, which is important for a large class of graph rewrite systems. In addition, we show that \pbpostrong is well-suited for rewriting labeled graphs and certain classes of attributed graphs. For this purpose, we employ a lattice structure on the label set and use order-preserving graph morphisms. We argue that our approach is simpler and more general than related relabeling approaches in the lite…

A Generalized Concurrent Rule Construction for Double-Pushout Rewriting

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 it: The sequential application of two rules can equivalently be replaced by the application of a concurrent rule and vice versa. We extend and generalize this result by introducing generalized concurrent rules (GCRs). Their distinguishing property is that they allow identifying and preserving elements that are deleted by their first underlying rule and crea…

Rewriting Theory for the Life Sciences: A Unifying Theory of CTMC Semantics (Long version)

The Kappa biochemistry and the MØD organic chemistry frameworks are amongst the most intensely developed applications of rewriting-based methods in the life sciences to date. A typical feature of these types of rewriting theories is the necessity to implement certain structural constraints on the objects to be rewritten (a protein is empirically found to have a certain signature of sites, a carbon atom can form at most four bonds, ...). In this paper, we contribute a number of original developments that permit to implement a universal theory of continuous-time Markov chains (CTMCs) for stochas…

用右平坦规则模置换理论重写的终止

Termination of Rewriting with Right-Flat Rules Modulo Permutative Theories

我们提出了可判定性的结果终止类的长期重写系统模置换理论。终端和最里面的终止模置换理论被证明是可判定的长期重写系统（TRS），其右手边的条款被限制为浅（变量发生在深度最多一个）和线性（每个变量发生在最多一次）。最内层终止模置换理论也被证明是可判定的浅TRS。我们首先表明，一个浅TRS可以转化为一个平面（只有变量和常数发生在深度1）TRS，同时保持终止和最内层终止。然后证明了可判定性的结果表明：（a）右平坦右线性（平坦）TRS，非终止（分别，最内非终止）意味着从平坦项开始的非终止，和（b）右平坦TRS，从给定项开始的非终止导子的存在是可判定的。在消极的一面，我们显示PSPACE-硬的终止和最内终止浅右线性TRS，和undecidability终止平坦的TRS。