zbMATH — the first resource for mathematics

Using unavoidable set of trees to generalize Kruskal’s theorem. (English) Zbl 0676.06003
Termination is an important property for term rewriting systems. To prove termination, 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 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.

06A06 Partial orders, general
68Q65 Abstract data types; algebraic specification
05C05 Trees
68W30 Symbolic computation and algebraic computation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Dershowitz, N., Ordering for term rewriting systems, Theoretical computer science, 17, 279-300, (1982) · Zbl 0525.68054
[2] Erhenfeucht, A.; Haussler, D.; Rozenberg, G., On regularity of context-free languages, Theoretical computer science, 27, 311-332, (1983) · Zbl 0553.68044
[3] Higman, G., Ordering by divisibility in abstract algebra, Proc. London math. soc., 3, 2, 326-336, (1952) · Zbl 0047.03402
[4] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J.a.c.m., 27, 797-821, (1980) · Zbl 0458.68007
[5] Kruskal, J.B., Well quasi-ordering, the tree theorem and Vazsonyi’s conjecture, Trans. AMS, 95, 210-225, (1960) · Zbl 0158.27002
[6] Kruskal, J.B., The theory of well quasi-ordering: A frequently discovered concept, J. combin. theory, 13, ser A, 297-305, (1972) · Zbl 0244.06002
[7] Kamin, S.; Lévy, J.J., Two generalizations of the recursive path ordering, (February 1980), Department of computer science, University of Illinois Urbana, IL, Unpublished note
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.