The DP framework for proving termination of term rewriting [Elektronische Ressource] / vorgelegt von René Thiemann. [RWTH Aachen, Department of Computer Science]

Sujets

• Informatik

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2007
• Nombre de lectures: 3
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Aachen
Department of Computer Science
Technical Report
The DP Framework for Proving
Termination of Term Rewriting
Ren´e Thiemann
ISSN 0935–3232 · Aachener Informatik Berichte · AIB-2007-17
RWTH Aachen · Department of Computer Science · October 2007The publications of the Department of Computer Science of RWTH Aachen (Aachen
University of Technology) are in general accessible through the World Wide Web.
http://aib.informatik.rwth-aachen.de/The DP Framework for Proving Termination
of Term Rewriting
Von der Fakult¨at fur¨ Mathematik, Informatik und
Naturwissenschaften der Rheinisch-Westf¨alischen
Technischen Hochschule Aachen zur Erlangung des
akademischen Grades eines Doktors der
Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Informatiker
Ren´e Thiemann
aus
Stadtlohn
Berichter: Prof. Dr. Jurgen¨ Giesl
Prof. Dr. Aart Middeldorp
Tag der mundlic¨ hen Prufung¨ : 24.10.2007
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online verfu¨gbarAbstract
Termination is the fundamental property of a program that for each input, the evalua-
tion will eventually stop and return some output. Although the question whether a given
program terminates is undecidable, many techniques have been developed which can be
used to answer the question of termination for many programs automatically. Especially,
termination of term rewriting is an interesting and widely studied area: Since the basic
evaluation mechanism of many programming languages is term rewriting, one can suc-
cessfully apply the termination techniques for term rewriting to analyze termination of
programs automatically. Nevertheless, there still remain many programs that cannot be
handled by any current technique that is amenable to automation
In this thesis, we extend existing techniques and develop new methods for mechanized
termination analysis of term rewrite systems. Currently, one of the most powerful tech-
niques is the dependency pair approach. Up to now, it was regarded as one of several
possible methods to prove termination. We show that dependency pairs can instead be
used as a general concept to integrate arbitrary techniques for termination analysis. In
this way, the benefits of different techniques can be combined and their modularity and
power are increased significantly. We refer to this new concept as the “dependency pair
framework” to distinguish it from the old “dependency pair approach”.
Moreover, this framework facilitates the development of new methods for termination
analysis. To demonstrate this, we design several novel techniques within the dependency
pair framework. They can successfully be applied to prove termination of previously
challengingprograms. Forexample, ourworkdescribesnewwayshowtohandleprograms
using accumulators, programs written in higher-order languages, and programs which
only terminate w.r.t. a given evaluation strategy. We additionally show how to disprove
termination, even under strategies.
All presented techniques are formulated in a uniform setting and are implemented in
our fully automated termination prover AProVE. The significance of our results is demon-
strated at the annual international Termination Competition, where the leading auto-
mated tools try to analyze termination of programs from different areas of computer
science: Without the contributions of this thesis, AProVE would not have reached the
highest scores both for proving and disproving termination in the years 2004 – 2007.Acknowledgments
Zuallererst m¨ochte ich mich bei Prof. Dr. Jurgen¨ Giesl bedanken. Seit meiner Zeit am
Lehr- und Forschungsgebiet hat er mich in jeder erdenklichen Weise unterstut¨ zt, sei es
durch die vielen interessanten Anregungen und Diskussionen, durch die gemeinsame Ar-
beit bei der Entwicklung neuer Papiere, durch die Freiheit, meinen Arbeitsschwerpunkt
sowohl thematisch als auch geographisch weitestgehend frei zu w¨ahlen, oder durch die
Unterstut¨ zung zum Umgang mit den “Kleinen” Freuden des privaten Lebens.
I am grateful to Prof. Dr. Aart Middeldorp for being a member of my thesis committee,
and for being a stimulating adversary in developing techniques for termination proving.
Ich danke vor allem auch meinem Kollegen Peter Schneider-Kamp. Zusammen mit ihm
gab es immer wieder neue interessante Ideen zu diskutieren und zu entwickeln, und ich
hoffe,nichtnurichhabeesgenossen,selbstdieabschreckendstenBeweisezurgegenseitigen
¨Uberprufung¨ auszutauschen. Zudem h¨atte ich ohne ihn wohl so manche halbe Stunde
h¨aufiger am Bahnhof gesessen.
Ich danke auch meinen Kollegen Stephan Swiderski und Carsten Fuhs fur¨ so manches
interessante Gespr¨ach und fur¨ das Korrekturlesen meiner Dissertation.
Thanks are given to everybody on the floor of I2 for a pleasant and friendly research
environment.
Vielen Dank geht auch an die restlichen Mitglieder des AProVE-Teams. Ohne ihre Un-
terstutzung¨ h¨atten kaum so viele Techniken vom Papier auf den Rechner gebracht werden
k¨onnen. Zudem haben die vielen guten Ideen bei der Implementierung mit Sicherheit
einen nicht unbeachtlichen Teil zum Erfolg bei den Wettbewerben beigetragen.
Und natur¨ lich will ich mich auch bei Karin bedanken. Obwohl ich vor mehreren Dead-
lines kaum fur¨ sie ansprechbar war, hat sie mich immer unterstutzt¨ und mir Ruc¨ khalt
gegeben.
Ren´e ThiemannContents
1. Introduction 1
2. The Dependency Pair Framework 7
2.1. Q-Restricted Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2. Dependency Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
3. Processors Without Search 17
3.1. Dependency Graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.2. Switching to Innermost Termination . . . . . . . . . . . . . . . . . . . . . 24
3.3. Usable Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.4. Star-Estimation of the Dependency Graph . . . . . . . . . . . . . . . . . . 31
3.5. ReducingQ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4. Processors Based on Orders 37
4.1. Reduction Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2. Needed Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.3. Rule Removal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.4. Usable Rules w.r.t. an Argument Filter . . . . . . . . . . . . . . . . . . . . 54
4.5. Needed Rules w.r.t. an Argument Filter. . . . . . . . . . . . . . . . . . . . 56
4.6. Subterm Criterion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
5. Processors Based on Pair Transformations 67
5.1. Instantiation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.2. Forward Instantiation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
5.3. Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
5.4. Narrowing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6. Processors for Applicative Rewriting 85
6.1. From Applicative to Functional Form . . . . . . . . . . . . . . . . . . . . . 87
6.2. Needed Rules for Applicative DP Problems . . . . . . . . . . . . . . . . . . 93
6.3. Argument Filters for Applicative DP Problems . . . . . . . . . . . . . . . . 97
7. Processors Based on Semantic Labeling 105
7.1. Semantic Labeling with Models . . . . . . . . . . . . . . . . . . . . . . . . 105
7.2.tic Labeling with Quasi-Models . . . . . . . . . . . . . . . . . . . . . 113
7.3. Semantic Labeling and Unlabeling . . . . . . . . . . . . . . . . . . . . . . . 120
8. Processors for Non-Termination Analysis 129
8.1. Looping Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130
8.2. Switching to Termination. . . . . . . . . . . . . . . . . . . . . . . . . . . . 133
8.3. Detecting Looping Problems . . . . . . . . . . . . . . . . . . . . . . . . . . 135II Contents
9. Conclusion 143
Bibliography 149
A. Proofs 159
A.2. Proofs of Chapter 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 159
A.3. Proofs of 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160
A.4. Proofs of Chapter 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
A.5. Proofs of 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
A.6. Proofs of Chapter 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182
A.7. Proofs of 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190
A.8. Proofs of Chapter 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194
List of Processors 201
Index 203