Loading...
Please wait, while we are loading the content...
Similar Documents
Automatic proofs of termination of context-sensitive rewriting
| Content Provider | Semantic Scholar |
|---|---|
| Author | Gil, Raúl Gutiérrez |
| Copyright Year | 2010 |
| Abstract | The idea of an incremental application of different termination techniques as processors for solving termination problems has shown to be a powerful and efficient way to prove termination of rewriting. Nowadays, the dependency pair framework (which develops this idea) is the most successful approach for proving termination of rewriting. The dependency pair framework relies on the notion of dependency pair to decompose a termination problem into a set of dependency pair problems. These dependency pair problems can be treated independently by applying different dependency pair processors. If we prove (disprove) the finiteness of all (some) of the dependency pair problems, then we can ensure that the system is terminating (nonterminating). This simple but powerful schema is the basis of state-of-art tools for automatically proving termination of rewriting. Context-sensitive rewriting [Luc98, Luc02] is a restriction of rewriting that forbids reductions on some subexpressions and that has proven to be useful in modeling and analyzing programming language features at different levels. In particular, termination of context-sensitive rewriting has proven to be useful in analyzing and proving termination of programs in several programming languages and variants of term rewriting. Over the last fifteen years, a number of techniques for proving termination of context-sensitive rewriting have been developed and implemented (essentially transformations and appropriate orderings). However, the definition of a context-sensitive dependency pair framework started only four years ago, when the research developed in this thesis began. In this thesis, we show how to develop a dependency pair framework for proving termination of context-sensitive rewriting. We also provide experimental evidence of the advantages of the context-sensitive dependency pair framework in the development of tools for automatically proving termination of context-sensitive rewriting. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.dsic.upv.es/docs/bib-dig/tesis/etd-06302010-130033/Thesis.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
