Hyperedge replacement jungle rewriting for term-rewriting systems and logic programming (Q685465)

The paper presents a graph rewriting formalisms (called Hyperedge Replacement (HR) Jungle Rewriting) based on the algebraic approach to graph rewriting, where a rewriting step is modelled by a double-pushout construction. The considered graphs are called jungles, and are shown to be suitable to represent (collections of) terms over a multisorted signature; moreover, graph morphisms model substitutions. Jungles are therefore hypergraphs essentially equivalent to directed acyclic graphs (dags). The rewriting mechanism is restricted to hyperedge replacement, i.e., at most one hyperedge can be replaced by a jungle at each derivation step. The original point (w.r.t. the work on Jungle Evaluation in [\textit{A. Habel}, \textit{H.-J. Kreowski} and \textit{D. Plump}, Jungle evaluation, in Fundamenta Informaticae 15(1), 37-60 (1991; Zbl 0727.68061)]) is that rewriting (i.e., the double-pushout construction) is performed in the category of jungles, and not in the bigger category of hypergraphs. The consequence is that, despite the restriction to hyperedge replacement, the resulting rewriting formalism is strictly more powerful, as it is able to model not only term rewriting systems, but also logic programming. This result relies upon the fact that in the category of jungles the pushout of two arrows corresponds to the most general unifier of two substitutions. The paper shows how term rewrite rules and logic programming clauses can be transformed into HR jungle rules. The main theorems state the soundness of these translations (i.e., the jungle rule representing a term rewrite rule (a program clause) can be applied to a jungle only if the original rule (clause) can be applied to the term (goal) represented by the jungle); the completeness of the translation of logic programs (if a clause can be applied to a goal, the corresponding jungle rule can be applied to any jungle representing the goal, yielding equivalent results); and the completeness w.r.t applicability of the translation of term rewriting systems (i.e., if a rule is applicable to a term, so is the corresponding jungle rule to any jungle representing the term). The results compare favourably with related results in the literature. In fact, to our knowledge, all the proposed approaches to term graph rewriting (both those using the algebraic approach and the others) fail to satisfy the completeness w.r.t. applicability for non-left-linear rules: often these are treated in ad hoc way. Moreover, unlike HR Jungle Rewriting, none of those approaches can be exploited to handle logic programming in a uniform way.