[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jean-Claude Raoult
Date: June 1993
Summary: Find an embedding theorem for directed graphs.
Termination is, as we know, undecidable. Yet, there are several sufficient conditions ensuring termination for word and term rewritings. Most are suitable extensions of Higman’s or Kruskal’s embeddings [Kru60]. Robertson and Seymour [RS] have achieved a similar theorem for undirected graphs. However, no embedding theorem has yet been proved for directed graphs, and (consequently?) powerful termination orderings remain to be designed.
This problem is related to Problem #100.
In [RS96], embedding theorems are proved for directed wqo-labelled graphs and hypergraphs.
Date: Mon, 31 Jan 2005 10:20:21 +0100
Graph rewriting termination: it is usually no problem because there is no duplication of subgraph, and the size reduces. One can of course interpret a term rewriting system as a graph rewriting system, if the symbols of the term denote graph operations. Hence, the termination is handled at the level of terms, with the well-known tools and criteria.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |