← All problems
Unverified

How can termination orderings for term rewriting be adapted to cover those cases in which graph rewriting is terminating although term rewriting is not?

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

Graph rewriting systems that implement term rewriting systems (see, for example, [D. Plump, 1993]) are terminating whenever term rewriting is. The converse, however, does not hold [D. Plump, 1993]. How can termination orderings for term rewriting be adapted to cover those cases in which graph rewriting is terminating although term rewriting is not?

It would be interesting to see an example not too artificial where the termination proof is difficult. Graph rewriting systems implementing term rewriting do not duplicate subgraphs. So the major source of difficulty in termination proofs disappears.

Recorded update.

Submitted by Klaus Guenter Dabisch on Mon Mar 9 13:44:57 MET 1998.

This problem was solved intuitively in [D. Plump, 1993]. One could solve the difficult termination proofs in this way: The Gross-Knuth reduction is defined by: Contract all redexes simultaneously [D. Plump, 1993]. Then, however, one has to prove that the result is unequivocal.

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu