Static termination analysis for Prolog using term rewriting and SAT solving

Schneider-Kamp, Peter; Giesl, Jürgen

doi:0935-3232

Static termination analysis for Prolog using term rewriting and SAT solving = Statische Terminierungsanalyse für Prolog unter Verwendung von Termersetzung und SAT-Lösern

Schneider-Kamp, Peter (Author)

2008

Verantwortlichkeitsangabevorgelegt von Peter Schneider-Kamp

ImpressumAachen : Publikationsserver der RWTH Aachen University 2008

UmfangII, 174 S. : graph. Darst.

ReiheAachener Informatik-Berichte ; 2008,17

Zugl.: Aachen, Techn. Hochsch., Diss., 2008

Zsfassung in engl. und dt. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2008-12-08

Online
URN: urn:nbn:de:hbz:82-opus-26300
URL: https://publications.rwth-aachen.de/record/63748/files/Schneider_Kamp_Peter.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Terminierung <Informatik> (Genormte SW) ; PROLOG <Programmiersprache> (Genormte SW) ; Termersetzungssystem (Genormte SW) ; Erfüllbarkeitsproblem (Genormte SW) ; Automatisches Beweisverfahren (Genormte SW) ; Verifikation (Genormte SW) ; Informatik (frei) ; termination (frei) ; logic programming (frei) ; term rewriting (frei) ; SAT (frei) ; automated reasoning (frei) ; verification (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Das fundamentalste Entscheidungsproblem in der Informatik ist das Halteproblem, das heißt gegeben ein Programm und eine Eingabe, entscheide ob das Programm nach endlich vielen Schritten hält, oder ob es auf dieser Eingabe endlos läuft. Obwohl Turing gezeigt hat, dass dieses Problem im Allgemeinen unentscheidbar ist, ist die Entwicklung von statischen Analysetechniken, die automatisch Terminierung für viele Programme und Eingaben beweisen können, von großem praktischen Interesse. Dies gilt insbesondere für die Logikprogrammierung, da die inhärente ungerichtete Berechnung quasi garantiert, dass jedes nicht-triviale Programm nur für bestimmte Eingaben terminiert. Aus diesem Grund ist die Terminierung von Logikprogrammen ausführlich untersucht worden, und in den letzten Jahrzehnten sind deutliche Fortschritte gemacht worden. Heutzutage gibt es vollautomatisierte Tools, die versuchen die Terminierung eines Logikprogramms im Hinblick auf eine gegebene Klasse von Eingaben zu Untersuchen. Trotzdem gibt es noch viele Logikprogramme, deren Terminierung von keiner aktuellen Terminierungstechnik, die gut automatisierbar ist, gezeigt werden kann. Ein anderes Gebiet, in dem Terminierung sogar noch intensiver untersucht wurde, ist Termersetzung. Dieses grundlegende Berechnungsprinzip ist die Grundlage der Auswertungsmechanismen vieler Programmiersprachen. Signifikante Fortschritte in Richtung auf mächtige, automatisierbare Terminierungstechniken während des letzten Jahrzehnts haben eine Menge von mächtigen Tools für die automatische Terminierungsanalyse hervorgebracht. In dieser Dissertation wird gezeigt, dass Techniken, die für die Terminierungsanalyse von Termersetzung entwickelt wurden, erfolgreich für Logikprogrammierung angepasst und angewendet werden können. Die neuentwickelten Techniken erweitern die Anwendbarkeit und die Mächtigkeit automatischer Terminierungsanalyse von Logikprogrammen signifikant. Die hier präsentierten Beiträge reichen von der Adaption von Techniken für die direkte Anwendung auf Logikprogramme bis zu Transformationen von Logikprogrammen in eine spezialisierte Form der Termersetzung. Im Bereich der Logikprogrammierung wird außerdem ein neuer Vorverarbeitungsansatz vorgestellt, um Logikprogramme mit Cuts analysieren zu können. Im Bereich der Termersetzung wird gezeigt, wie man für bestimmte beliebte Klassen von fundierten Ordnungen auf Termen diese effizienter durch eine Kodierung in aussagenlogische Erfüllbarkeitsprobleme finden kann. Die Beiträge dieser Dissertation sind in Tools zur automatischen Terminierungsanalyse implementiert – hauptsächlich in unserem vollautomatischen Tool AProVE. Die Bedeutung unserer Resultate wird durch die Tatsache, dass AProVE sowohl in Termersetzung als auch in Logikprogrammierung bei allen internationalen Terminierungswettbewerben seit 2004 die höchste Punktzahl erreicht hat, verdeutlicht. Bei diesen Wettbewerben versuchen die führenden automatisierten Tools die Terminierung von Programmen aus verschiedenen Gebieten der Informatik zu untersuchen.

The most fundamental decision problem in computer science is the halting problem, i.e., given a description of a program and an input, decide whether the program terminates after finitely many steps or runs forever on that input. While Turing showed this problem to be undecidable in general, developing static analysis techniques that can automatically prove termination for many pairs of programs and inputs is of great practical interest. This is true in particular for logic programming, as the inherent lack of direction in the computation virtually guarantees that any non-trivial program terminates only for certain classes of inputs. Thus, termination of logic programs is widely studied and significant advances have been made during the last decades. Nowadays, there are fully-automated tools that try to prove termination of a given logic program w.r.t. a given class of inputs. Nevertheless, there still remain many logic programs that cannot be handled by any current termination technique for logic programs that is amenable to automation. Another area where termination has been studied even more intensively is term rewriting. This basic computation principle underlies the evaluation mechanism of many programming languages. Significant advances towards powerful automatable termination techniques during the last decade have yielded a plethora of powerful tools for proving termination automatically. In this thesis, we show that techniques developed for proving termination of term rewriting can successfully be adapted and applied to analyze logic programs. The new techniques developed significantly extend the applicability and the power of automated termination analysis for logic programs. The work presented here ranges from adapting techniques to work directly on logic programs to transformations from logic programs to a specialized version of term rewriting. On the logic programming side we also present a new pre-processing approach to handle logic programs with cuts. On the term rewriting side we show how to search for certain popular classes of well-founded orders on terms more efficiently by encoding the search into satisfiability problems of propositional logic. The contributions developed in this thesis are implemented in tools for automated termination analysis – mostly in our fully automated termination prover AProVE. The significance of our results is demonstrated by the fact that AProVE has reached the highest score both for term rewriting and logic programming at the annual international Termination Competitions in all years since 2004, where the leading automated tools try to analyze termination of programs from different areas of computer science.

Fulltext:
PDF