Graph Path Orderings

19 pages•Published: October 23, 2018

Nachum Dershowitz and Jean-Pierre Jouannaud

Abstract

We define well-founded rewrite orderings on graphs and show that they can be used to show termination of a set of graph rewrite rules by verifying all their cyclic extensions. We then introduce the graph path ordering inspired by the recursive path ordering on terms and show that it is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our ordering applies to arbitrary finite, directed, labeled, ordered multigraphs, hence provides a building block for rewriting with graphs, which should impact the many areas in which computations take place on graphs.

Keyphrases: cyclic graphs, graph rewriting, multigraphs, path orderings, rewrite orderings, termination

In: Gilles Barthe, Geoff Sutcliffe and Margus Veanes (editors). LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol 57, pages 307-325.

Links:	https://easychair.org/publications/paper/8DzT
	https://doi.org/10.29007/6hkk

BibTeX entry

@inproceedings{LPAR-22:Graph_Path_Orderings,
  author    = {Nachum Dershowitz and Jean-Pierre Jouannaud},
  title     = {Graph Path Orderings},
  booktitle = {LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  editor    = {Gilles Barthe and Geoff Sutcliffe and Margus Veanes},
  series    = {EPiC Series in Computing},
  volume    = {57},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/8DzT},
  doi       = {10.29007/6hkk},
  pages     = {307-325},
  year      = {2018}}

Download PDF Open PDF in browser