Find an embedding theorem for directed graphs.

The source page states the original problem together with its recorded qualifications and progress updates as follows.

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 [Raoult, 1993]. Robertson and Seymour [Raoult, 1993] 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 RTALooP entry gap-embedding.

Recorded progress.

In [Raoult, 1993], embedding theorems are proved for directed wqo-labelled graphs and hypergraphs.

Recorded update.

Submitted by Bruno Courcelle on 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.