The relationship between Term Graph Rewriting and Term Rewriting is well understood: a single term graph reduction may correspond to several term reductions, due to sharing. It is also known that if term graphs are allowed to contain cycles, then one term graph reduction may correspond to infinitely many term reductions. We stress that this fact can be interpreted in two ways. According to the "sequential interpretation", a term graph reduction corresponds to an infinite sequence of term reductions, as formalized by Kennaway et.al. using strongly converging derivations over the complete metric space of infinite terms. Instead according to the "parallel interpretation" a term graph reduction corresponds to the parallel reduction of an infinite set of redexes in a rational term. We formalize the latter notion by exploiting the complete partial order of infinite and possibly partial terms, and we stress that this interpretation allows to explain the result of reducing circular redexes in several approaches to term graph rewriting.
We study rewriting systems whose underlying set of terms is equipped with a vector space structure over a given field. We introduce parallel rewriting relations, which are rewriting relations compatible with the vector space structure, as well as rewriting strategies, which consist in choosing one rewriting step for each reducible basis element of the vector space. Using these notions, we introduce the S-confluence property and show that it implies confluence. We deduce a proof of the diamond's lemma, based on strategies. We illustrate our general framework with rewriting systems over rational…
In order to define graph transformations by the simultaneous application of concurrent rules, we have adopted in previous work a structure of attributed graphs stable by unions. We analyze the consequences on parallel independence, a property that characterizes the possibility to resort to sequential rewriting. This property turns out to depend not only on the left-hand side of rules, as in algebraic approaches to graph rewriting, but also on their right-hand side. It is then shown that, of three possible definitions of parallel rewriting, only one is convenient in the light of parallel indepe…
Encodings of term rewriting systems (TRSs) into graph rewriting systems usually lose global termination, meaning the encodings do not terminate on all graphs. A typical encoding of the terminating TRS rule a(b(x)) -> b(a(x)), for example, may be indefinitely applicable along a cycle of a's and b's. Recently, we introduced PBPO+, a graph rewriting formalism in which rules employ a type graph to specify transformations and control rule applicability. In the present paper, we show that PBPO+ allows for a natural encoding of linear TRS rules that preserves termination globally. This result is a st…
The basic principle of graph rewriting is the stepwise replacement of subgraphs inside a host graph. A challenge in such replacement steps is the treatment of the patch graph, consisting of those edges of the host graph that touch the subgraph, but are not part of it. We introduce the patch graph rewriting framework, a visual graph rewriting language with precise formal semantics. The language has rich expressive power in two ways. Firstly, rules can flexibly constrain the permitted shapes of patches touching matching subgraphs. Secondly, rules can freely transform patches. While the framework…
Term graph rewriting is important as "conceptual implementation" of the execution of functional programs, and of data-flow optimisations in compilers. One way to define term graph transformation rule application is via the well-established and intuitively accessible double-pushout (DPO) approach; we present a new result proving semantics preservation for such DPO-based term graph rewriting.
We tackle the problem of attributed graph transformations and propose a new algorithmic approach for defining parallel graph transformations allowing overlaps. We start by introducing some abstract operations over graph structures. Then, we define the notion of rewrite rules as three inclusions of the form $L \supseteq K \supseteq M \subseteq R$. We provide six conditions that parallel graph rewrite relations should ideally satisfy, which lead us to define two distinct full parallel graph rewrite relations. A central notion of regularity of matchings is proved to be equivalent to these six con…
We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. The applicability and the precision of the method are demonstrated by the relatively light effort in extending the program analysis tool AProVE and by experiments on numerous benchmarks from the literature.
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…
We provide a tutorial introduction to the algebraic graph rewriting formalism PBPO+. We show how PBPO+ can be obtained by composing a few simple building blocks, and model the reduction rules for binary decision diagrams as an example. Along the way, we comment on how alternative design decisions lead to related formalisms in the literature, such as DPO. We close with a detailed comparison with Bauderon's double pullback approach.
On Complexity Bounds and Confluence of Parallel Term Rewriting
LIP (UMR CNRS/ENS Lyon/UCB Lyon1/Inria)（LIP（法国国家科学研究中心/里昂高等师范学院/里昂第一大学/法国国家信息与自动化研究所联合研究单位））；Birkbeck, University of London（伦敦大学伯贝克学院）；University Grenoble Alpes（格勒诺布尔阿尔卑斯大学）
We tackle the problem of simultaneous transformations of networks represented as graphs. Roughly speaking, one may distinguish two kinds of simultaneous or parallel rewrite relations over complex structures such as graphs: (i) those which transform disjoint subgraphs in parallel and hence can be simulated by successive mere sequential and local transformations and (ii) those which transform overlapping subgraphs simultaneously. In the latter situations, parallel transformations cannot be simulated in general by means of successive local rewrite steps. We investigate this last problem in the fr…
The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in particular partial map classifiers, in a topos. Second, we introduce an extension by enriching objects with annotations and give a precise characterization of strongest post-conditions, which are effec…
We introduce proof terms for string rewrite systems and, using these, show that various notions of equivalence on reductions known from the literature can be viewed as different perspectives on the notion of causal equivalence. In particular, we show that permutation equivalence classes (as known from the lambda-calculus and term rewriting) are uniquely represented both by trace graphs (known from physics as causal graphs) and by so-called greedy multistep reductions (as known from algebra). We present effective maps from the former to the latter, topological multi-sorting TM, and vice versa, …
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…
Motivated by questions from program transformations, eight notions of isomorphisms between term rewriting systems are defined, analysed, and classified. The notions include global isomorphisms, where the renaming of variables and function symbols is the same for all term rewriting rules of the system, local ones, where a single renaming for every rule is used, and a combination, where one symbol set is renamed globally while the other set is renamed locally. Preservation of semantic properties like convertibility and termination is analysed for the different isomorphism notions. The notions of…
In implementing evaluation strategies of the lambda-calculus, both correctness and efficiency of implementation are valid concerns. While the notion of correctness is determined by the evaluation strategy, regarding efficiency there is a larger design space that can be explored, in particular the trade-off between space versus time efficiency. We contributed to the study of this trade-off by the introduction of an abstract machine for call-by-need, inspired by Girard's Geometry of Interaction, a machine combining token passing and graph rewriting. This work presents an extension of the machine…
We consider recognizable trace rewriting systems with level-regular contexts (RTL). A trace language is level-regular if the set of Foata normal forms of its elements is regular. We prove that the rewriting graph of a RTL is word-automatic. Thus its first-order theory is decidable. Then, we prove that the concurrent unfolding of a finite concurrent automaton with the reachability relation is a RTL graph. It follows that the first-order theory with the reachability predicate (FO[Reach] theory) of such an unfolding is decidable. It is known that this property holds also for the ground term rewri…
Graph transformation is the rule-based modification of graphs, and is a discipline dating back to the 1970s. The declarative nature of graph rewriting rules comes at a cost. In general, to match the left-hand graph of a fixed rule within a host graph requires polynomial time. To improve matching performance, Dörr proposed to equip rules and host graphs with distinguished root nodes. This model was implemented by Plump and Bak, but unfortunately, is not invertible. We address this problem by defining rootedness using a partial function onto a two-point set rather than pointing graphs with root …
Graph rewrite formalisms are a powerful approach to modeling complex molecular systems. They capture the intrinsic concurrency of molecular interactions, thereby enabling a formal notion of mechanism (a partially ordered set of events) that explains how a system achieves a particular outcome given a set of rewrite rules. It is then useful to verify whether the mechanisms that emerge from a given model comply with empirical observations about their mutual interference. In this work, our objective is to determine whether a specific event in the mechanism for achieving X prevents or promotes the …
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 account of a concurrency theorem for this important type of rewriting, and we demonstrate the additional mathematical property of a form of associativity for these theories. Associativity may then be exploited to construct so-called rule algebras (of SqPO type), based upon which in particular a universal framework of continuous-time Markov chains for stochastic Sq…
In this paper, we study how graph transformations based on sesqui-pushout rewriting can be reversed and how the composition of rewrites can be constructed. We illustrate how such reversibility and composition can be used to design an audit trail system for individual graphs and graph hierarchies. This provides us with a compact way to maintain the history of updates of an object, including its multiple versions. The main application of the designed framework is an audit trail of updates to knowledge represented by hierarchies of graphs. Therefore, we introduce the notion of rule hierarchy that…
An algorithm is in-place, or runs in-situ, when it does not need any additional memory to execute beyond a small constant amount. There are many algorithms that are efficient because of this feature, therefore it is an important aspect of an algorithm. In most programming languages, it is not obvious when an algorithm can run in-place, and moreover it is often not clear that the implementation respects that idea. In this paper we study interaction nets as a formalism where we can see directly, visually, that an algorithm is in-place, and moreover the implementation will respect that it is in-p…
