文档介绍：J. putation (1989) 8, 335-382
Using Unavoidable Set of Trees to Generalize Kruskal's Theorem
Laurence Puel
Wraroire&IMonrrPa'qu de I'Ecdr Norm& Sqhkure
URh 1327
45 rue dUh, 75005 Paris.
INTRODUCTION
Termination is an important property for term rewriting systems. To prove termination,
[I] introduces quasi-simplification orderings that are monotonic extensions of the
embedding relation. He proves that they are well quasi-ordered and a fortiori well-founded by
using a theorem from Kruskal[5]. which shows that the simple nee insertion order TIO (defined
below) is a well quasi-ordering over a certain set of trees. (Well-founded means that every
nonempty set contains at least one minimal element; well quasi-ordered means that every
nonempty set contains at least one and at most a finite number of parable minimal
elements.) Dershowitz's method is powerful, but cannot be used when the rewriting system
contains a rule whose right hand side is embedded in the left hand side. The purpose of this
paper is to e this constraint, when the rewriting system uses a frnite ranked alphabet, by
generalizing Kruskal's theorem to obtain a family of quasi-orders TIO(S, 61) that are strictly
included in TI0 but are still well quasiah. This generalization is parallel to the generahation
described in the next paragraph.
G. Higman [3] includes a well-known subsidiary result. Theorem , which has the
following result as a special case: The set of all words Z* over the finite alphabet Z is well
quasi-ordered by the simple word insertion order WIO. The relation t WIO t' means that word t'
can be obtained from word t by inserting arbitrary words anywhere in t, including at the very
0747-7171/89/100335+48 (B 1989 Academic Press Limited
336 L. Puel
beginning and the very end. A. Ehrenfeucht, D. Haussler, and G. Rozenberg [2] have
generalized this result, and obtain a well quasi-order by permitting only words from a