Loading...
Please wait, while we are loading the content...
Similar Documents
Total Termination of Term Rewriting is Undecidable (1995)
| Content Provider | CiteSeerX |
|---|---|
| Author | Zantema, Hans |
| Abstract | Usually termination of term rewriting systems (TRS's) is proved by means of a monotonic well-founded order. If this order is total on ground terms, the TRS is called totally terminating. In this paper we prove that total termination is an undecidable property of finite term rewriting systems. The proof is given by means of Post's Correspondence Problem. 1 Introduction Termination of term rewriting systems (TRS's) is an important property. Often termination proofs are given by defining an order that is well-founded, and proving that for every rewrite step the value of the term decreases according this order. In many cases the order is monotonic, and it suffices to prove that l oe ? r oe for all rewrite rules l ! r and all ground substitutions oe. Standard techniques following this approach include recursive path order and Knuth-Bendix order, see for example [17]. It is an interesting question whether these orders are total or can be extended to a total monotonic order, or are essen... |
| File Format | |
| Volume Number | 20 |
| Journal | Journal of Symbolic Computation |
| Language | English |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Total Termination Term Rewriting Correspondence Problem Many Case Total Monotonic Order Termination Proof Rewrite Rule Interesting Question Ground Substitution Ground Term Recursive Path Order Finite Term Important Property Monotonic Well-founded Order Rewrite Step Undecidable Property Introduction Termination Knuth-bendix Order |
| Content Type | Text |
| Resource Type | Article |
