141 Pages
English

Automating recursive definitions and termination proofs in higher-order logic [Elektronische Ressource] / Alexander Krauss

Gain access to the library to view online
Learn more

Informations

Published by
Published 01 January 2009
Reads 23
Language English

Institut fur Informatik
der Technischen Universit at Munc hen
Automating Recursive De nitions and
Termination Proofs in Higher-Order Logic
Alexander Krauss
Vollst andiger Abdruck der von der Fakult at fur Informatik der Technischen
Universit at Munchen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
genehmigten Dissertation.
Vorsitzender: Univ.-Prof. Dr. Helmut Seidl
Prufer der Dissertation:
1. Univ.-Prof. Tobias Nipkow, Ph.D.
2. Prof. Lawrence C. Paulson, Ph.D.
University of Cambridge, UK
Die Dissertation wurde am 29.01.2009 bei der Technischen Universit at Munc hen
eingereicht und durch die Fakult at fur Informatik am 02.07.2009 angenommen.Abstract
The aim of this thesis is to provide an infrastructure for general recursive func-
tion de nitions in a proof assistant based on higher-order logic (HOL) that has
no native support for recursion or pattern matching.
In the rst part we develop a tool that automates recursive function de -
nitions and provides appropriate proof rules for them. Compared to previous
work, our package supports the de nition of partial functions, modeling the
domain of the function by an inductive domain predicate. An automatically-
generated partial induction rule makes partial correctness proofs independent
from termination proofs. This modularity considerably facilitates termination
arguments for nested recursions.
The second part addresses the problem of automatically solving the termi-
nation proof obligations that arise from function de nitions. Methods from the
literature can be applied, but require signi cant adaptation to the speci c needs
of our setting: They must produce full formal proofs and work relative to a rich
interactive theory. Our approach encompasses a rule-based selection of measure
functions, a simple control- ow analysis inspired by the dependency-pairs ap-
proach, and a modi ed version of the size-change principle based on certi cates.
A formalization of the full size-change principle is also provided.
In the third part we discuss how pattern matching, which occurs frequently
in functional programming, can be supported in HOL function de nitions. We
present a very general form of pattern matching, where arbitrary expressions
can serve as patterns. We show how such patterns can be encoded using a
custom matching combinator and how their consistency can be expressed in
proof obligations.
We also study the problem of transforming ML-style sequential pattern
matching into minimal sets of independent equations, such that they are con-
sistent in HOL. We relate the problem to the minimization problem for propo-
Psitional DNF formulas and show that it is -complete. We then develop a2
concrete algorithm that computes minimal patterns.
As another application of the new set of tools, we show how user-speci ed
induction schemes can be generated from simpler properties, which often makes
their proofs fully automatic.Zusammenfassung
Ziel dieser Arbeit ist die Entwicklung einer Infrastruktur fur rekursive Funk-
tionsde nitionen in einem interaktiven Theorembeweiser, in dem Rekursion und
Pattern-Matching nicht von Haus aus unterstutzt werden. Wir arbeiten im Kon-
text h oherstu ger Logik (higher-order logic, HOL).
Im ersten Teil entwickeln wir ein Werkzeug, welches Funktionsde nitionen
automatisiert und geeignete Beweisregeln dafur bereitstellt. Im Gegensatz zu
existierenden Ans atzen unterstutzt unser Verfahren auch partielle Funktionen,
die mit Hilfe eines induktiven Domainpr adikats modelliert werden. Eine au-
tomatisch generierte Induktionsregel erlaubt partielle Korrektheitsbeweise un-
abh angig von der Terminierung der Funktion. Diese modulare Struktur erle-
ichtert insbesondere die Behandlung von geschachtelter Rekursion.
Der zweite Teil behandelt automatische Terminierungsbeweise, um die aus
Funktionsde nitionen entstehenden Beweisverp ichtungen automatisch zuosen.l
Dabei verwenden wir Methoden aus der Literatur, die allerdings an die spezi s-
chen Anforderungen unseres Szenarios angepasst werden mussen. Unser Ansatz
beinhaltet eine regelbasierte Auswahl von Ma funktionen, eine einfache Kon-
troll ussanalyse ahnlich der Dependency-Pairs-Methode, und eine Variante des
Size-Change-Kriteriums mit Zerti katen. Eine Formalisierung des vollen Size-
Change-Kriteriums wird ebenfalls entwickelt.
Im dritten Teil untersuchen wir, wie das in der funktionalen Programmierung
gebr auchliche Pattern-Matching in HOL unterstutzt werden kann. Wir ent-
wickeln eine sehr allgemeine Form von Pattern-Matching in der Logik, welches
beliebige Terme als Patterns erlaubt und mit Hilfe eines speziellen Kombinators
in der Logik ausgedruc kt werden kann. Die Konsistenz der Spezi kation wird
durch spezielle Beweisverp ichtungen sichergestellt.
Au erdem untersuchen wir das Problem, Spezi kationen mit sequenziellem
Pattern-Matching in reine Gleichungsspezi kationen mit m oglichst wenigen Glei-
chungen umzuwandeln. Wir ziehen eine Parallele zum Problem der Minimierung
Boolescher Ausdruc ke in DNF und zeigen, dass das Minimierungsproblem fur
PPatterns -vollst andig ist. Wir geben auch einen konkreten Algorithmus zur2
Minimierung von Patterns an.
Als weitere Anwendung der neuen Werkzeuge zeigen wir, wie sich vom Be-
nutzer vorgegebene Induktionsschemata automatisch auf einfachere Beweisziele
reduzieren lassen, wodurch sich der Beweis solcher Schemata oft weitgehend
automatisierenasst.l To Katharina | with nonterminating loveAcknowledgements
I am deeply indebted to Tobias Nipkow for o ering me the opportunity to work
with him, and for being such a pleasant supervisor in every respect. He greatly
contributes to my education not only in logic and computer science, but also in
other areas, such as contemporary music. Working under his guidance is great
fun.
I am also grateful to Larry Paulson for agreeing to act as a referee and examiner,
and for creating the next 700 theorem provers.
I want to thank all present and former members of the Isabelle group at TUM
for making it such a fertile research biotope and such a friendly place. They
all in uenced this work in one or the other way: Clemens Ballarin, Stefan
Berghofer, Jasmin C. Blanchette, Sascha B ohme, Amine Chaieb, Florian Haft-
mann, Julien Narboux, Steven Obua, Norbert Schirmer, Christian Urban, Tjark
Weber, Makarius M. Wenzel, and Martin Wildmoser.
Jasmin and Makarius deserve special thanks for reading parts of this thesis and
decorating it with countless colourful annotations and corrections. Florian, who
shared the o ce with me in the beginning, has become something like a travel
companion on this journey (and various sub-journeys). I always enjoy being
exposed to his detailed knowledge of Bavarian history and his bizarre humour
| often both at the same time. Thanks are also due to Lukas Bulwahn and
Armin Heller, who worked on the implementation of the termination provers
described in Chapter 3. They did a very good job.
Finally I would like to thank the numerous users of Isabelle, without whom
much of this work would be meaningless.
My wife, Katharina Kuhn, provided moral support of all kinds during the whole
time, and especially in the end. I cannot thank her enough.
Parts of this research were nancially supported by DFG Project Ni 491/10-1.