Analysis of Graph Rewriting
Guillaume Bonfante, Bruno Guillaume, Guy Perrier · 2018
This chapter begins by establishing general properties for rewriting, a sort of toolbox for use in any more elaborate proofs. It provides examples of proof principles, such as induction. The chapter presents several proposals, which shows that rewriting is always correctly defined. It also provides a precise description of what can and cannot be computed with rewriting. The problem of non-uniform termination can be solved for rewriting without node creation. The technique for responding to the question of confluence broadly follows that used in term rewriting, and is based on Newman's lemma. The organization of computations is simpler for a confluent system. More significantly, some of the computations in question can, in fact, be carried out using a Turing machine. Turing machines act on words, while graph rewriting systems transform graphs. The chapter considers three criteria in the context of natural language processing: expressive capacity, simplicity and intentionality.