Abstract

In this extended abstract we study termination of term graph rewriting, where we restrict our attention to acyclic term graphs. More precisely, we establish a variant of Kruskal’s Tree Theorem formulated for term graphs. To this end we suitably adapt the original embedding relation on trees to a relation on directed, acyclic graphs. The proof then follows Nash-Williams’ minimal bad sequence argument.

BibTeX

@InProceedings{MS:2016a,
  author    = "Georg Moser and Maria A Schett",
  title     = "Kruskal's Tree Theorem for Term Graphs",
  booktitle = "Proceedings of the 9th International Workshop on Computing with
               Terms and Graphs (TERMGRAPH 2016)",
  year      = 2016
}