Convergence in infinitary term graph rewriting systems is simple

Term graph rewriting provides a formalism for implementing term rewriting in an efficient manner by emulating duplication via sharing. Infinitary term rewriting has been introduced to study infinite term reduction sequences. Such infinite reductions can be used to model non-strict evaluation. In this paper, we unify term graph rewriting and infinitary term rewriting thereby addressing both components of lazy evaluation: non-strictness and sharing. In contrast to previous attempts to formalise infinitary term graph rewriting, our approach is based on a simple and natural generalisation of the modes of convergence of infinitary term rewriting. We show that this new approach is better suited for infinitary term graph rewriting as it is simpler and more general. The latter is demonstrated by the fact that our notions of convergence give rise to two independent canonical and exhaustive constructions of infinite term graphs from finite term graphs via metric and ideal completion. In addition, we show that our notions of convergence on term graphs are sound w.r.t. the ones employed in infinitary term rewriting in the sense that convergence is preserved by unravelling term graphs to terms. Moreover, the resulting infinitary term graph calculi provide a unified framework for both infinitary term rewriting and term graph rewriting, which makes it possible to study the correspondences between these two worlds more closely.

C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions

We introduce a logic called C2PDLS, motivated by some reasoningabout graph rewriting systems. C2PDLS is an extension of bothcombinatory propositional dynamic logic, usually written CPDL,and converse propositional dynamic logic, usually written CPDLtoo. In addition to the existing features of both CPDLs, theintroduced logic offers the possibility to use the notion ofsubstitutions à la Hoare within its formulae. Such substitutionsreflect the effect of some actions on graph structures such asaddition or deletion of edges or nodes. These last features ledus to introduce restricted universal roles over subsets of theuniverse. We propose a sound and complete deductive system forC2PDLS and show that its validity problem is decidable.

Designing the Same, but in Different Ways: Determinism in Graph-Rewriting Systems for Function-Based Design Synthesis

This paper compares methods for identifying determinism within graph-rewriting systems. From the viewpoint of functional decomposition, these methods can be implemented to search efficiently for distinct function structures. An additional requirement is imposed on this comparison that stems from a cooperative design application where different organizations contribute to a distributed graph-rewriting system: Inspecting the definitions of production rules is not allowed for identifying determinism because production rules are considered to be confidential corporate knowledge. Under this assumption, two approaches were selected and empirically compared with respect to random search and guided search scenarios. The results suggest that the herein proposed dynamic rule independence analysis outperforms traditional approaches in light of the above restriction.