Using unavoidable set of trees to generalize Kruskal's theorem
Termination is an important property for term rewriting systems. To prove termination, \textit{N. Dershowitz} [Theor. Comput. Sci. 17, 279-301 (1982; Zbl 0525.68054)] 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 of \textit{J. B. Kruskal} [Trans. Am. Math. Soc. 95, 210-225 (1960; Zbl 0158.270)], which shows that the simple tree 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 noncomparable 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 overcome this constraint, when the rewriting system uses a finite ranked alphabet, by generalizing Kruskal's theorem to obtain a family of quasi-orders TIO(S,\(\omega)\) that are strictly included in TIO but are still well quasi-orders.
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- On regularity of context-free languages
- Ordering by Divisibility in Abstract Algebras
- Orderings for term-rewriting systems
- The theory of well-quasi-ordering: a frequently discovered concept
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
- Inventories of unavoidable languages and the word-extension conjecture
- What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
- Well rewrite orderings and well quasi-orderings
- On unavoidability of trees with k leaves
- Complexity bounds for some finite forms of Kruskal's theorem
- Well quasi-orders, unavoidable sets, and derivation systems
- Well Quasi-orders in Formal Language Theory
- scientific article; zbMATH DE number 3940739 (Why is no real title available?)
- Unavoidable languages, cuts and innocent sets of words
- A comparison of well-quasi orders on trees
- Kruskal's tree theorem for acyclic term graphs
- Embedding with patterns and associated recursive path ordering
- Generalizing Kruskal's theorem to pairs of cohabitating trees
- Linearizing well quasi-orders and bounding the length of bad sequences
- Well quasi-orders generated by a word-shuffle rewriting
This page was built for publication: Using unavoidable set of trees to generalize Kruskal's theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1122597)
