On the constructive content of proofs [Elektronische Ressource] / vorgelegt von Monika Seisenberger

Seisenberger, Monika

Sujets

• Mathematics

Informations

• Publié par: ludwig-maximilians-universitat_munchen
• Publié le: 01 janvier 2003
• Nombre de lectures: 10
• Langue: English

Extrait

On the Constructive Content of Proofs
Monika Seisenberger
Mun¨ chen 2003On the Constructive Content of Proofs
Monika Seisenberger
Dissertation
an der Fakult¨at fur¨ Mathematik und Informatik
der Ludwig–Maximilians–Universit¨at Munc¨ hen
vorgelegt von
Monika Seisenberger
M¨arz 2003Erstgutachter: Prof. Dr. H. Schwichtenberg
Zweitgutachter: Prof. Dr. W. Buchholz
Tag der mundlic¨ hen Prufung:¨ 10. Juli 2003Abstract
This thesis aims at exploring the scopes and limits of techniques for extract-
ing programs from proofs. We focus on constructive theories of inductive
definitions and classical systems allowing choice principles. Special emphasis
is put on optimizations that allow for the extraction of realistic programs.
Our main field of application is infinitary combinatorics. Higman’s Lemma,
having an elegant non-constructive proof due to Nash-Williams, constitutes
an interesting case for the problem of discovering the constructive content
behind a classical proof. We give two distinct solutions to this problem. First,
we present a proof of Higman’s Lemma for an arbitrary alphabet in a theory
of inductive definitions. This proof may be considered as a constructive
counterpart to Nash-Williams’ minimal-bad-sequence proof. Secondly, using
a refinedA-translation method, we directly transform the classical proof into
a constructive one and extract a program. The crucial point in the latter
is that we do not need to avoid the axiom of classical dependent choice but
directly assign a realizer to its translation.
A generalization of Higman’s Lemma is Kruskal’s Theorem. We present a
constructive proof of Kruskal’s Theorem that is completely formalized in a
theory of inductive definitions.
As a practical part, we show that these methods can be carried out in an
interactive theorem prover. Both approaches to Higman’s Lemma have been
implemented in Minlog.iiZusammenfassung
Ziel der vorliegenden Arbeit ist es, die Reichweiten und Grenzen von Tech-
niken zur Extraktion von Programmen aus Beweisen zu erforschen. Wir
konzentrieren uns dabei auf konstruktive Theorien Induktiver Definitionen
und klassische Systeme mit Auswahlprinzipien. Besonderes Gewicht liegt
auf Optimierungen, die zur Extraktion von realisischen Programmen fuhren.¨
Unser Hauptanwendungsgebiet ist die unendliche Kombinatorik. Higmans
Lemma, ein Satz mit einem eleganten klassischen, auf Nash-Williams zuruc¨ k-
gehenden Beweis, ist ein interessantes Fallbeispiel fur¨ die Suche nach dem
konstruktiven Gehalt in einem klassischen Beweis. Wir zeigen zwei unter-
schiedliche L¨ osungen zu dieser Problemstellung auf. Zun¨ achst pr¨ asentieren
wir einen induktiven Beweis von Higmans Lemma fur¨ ein beliebiges Alpha-
bet, der als konstruktives Pendant zum klassischen Beweis angesehen wer-
den kann. Als zweiten Ansatz verwandeln wir mit Hilfe der verfeinerten
¨A-Ubersetzungsmethode den klassischen Beweis in einen konstruktiven und
extrahieren ein Programm. Der entscheidende Punkt ist hierbei, dass wir
einen direkten Realisierer fur¨ das ub¨ ersetzte Auswahlaxiom verwenden.
Die Verallgemeinerung von Higmans Lemma fuhrt¨ zu Kruskals Satz. Wir
geben einen konstruktiven Beweis von Kruskals Theorem, der vollst¨ andig
auf den Induktiven Definitionen basiert.
Der praktische Teil der Arbeit befasst sich mit der Ausfuhrbark¨ eit dieser
Methoden und Beweise in dem Beweissystem Minlog.ivAcknowledgements
I wish to express my sincere thanks to Professor Helmut Schwichtenberg for
supervising this thesis and for providing and supporting a very lively scien-
tific environment. His constructive view of mathematical logic has widely
influenced this thesis. I thank him for his scientific advice, his patient guid-
ance and also the time he offered to me, not at least with extending the
Minlog system according to my needs and wishes.
I am grateful to my colleagues in the Munich working group and in the
Graduiertenkolleg ‘Logik in der Informatik’ for their interest and coopera-
tion during all the years. In particular, I want to thank Professor Wilfried
Buchholz for his advice concerning prooftheoretical questions, Felix Joachim-
ski for his continuous help in both mathematical and other matters, Laura
Crosilla for many stimulating discussions and her support, not only in pre-
senting this thesis, and Stefan Berghofer for his interest in implementations
of constructive proofs of Higman’s Lemma.
Many others have helped me with their comments and suggestions. I am
especially thankful to Professor Robert Constable for an encouraging dis-
cussion on the subject in Marktoberdorf, 2001, and to Daniel Fridlender for
sharing his knowledge on constructive proofs of Higman’s Lemma with me.
I am indebted to Professor John Tucker and the members of the Computer
Science Department of the University of Wales Swansea for integrating me
into a very strong theory group. Special thanks go to my colleagues Al-
Fathiatul Habibah Abdul Rahman, Marco Mazzucco and Will Harwood who
patiently answered all my questions concerning the English language.
My gratitude and my love go to Ulrich Berger. I thank him for his encour-
agement, his inspiring ideas and his overall support. Finally, I would like to
thank my friends and my two families for their benevolence and their support
to finish this work.
I gratefully acknowledge the support of the Graduiertenkolleg ‘Logik in der
Informatik’ sponsored by the Deutsche Forschungsgemeinschaft (DFG) and
the funding of the Engineering and Physical Sciences Research Council (EP-
SRC).CONTENTS
Contents
1 Introduction 1
1.1 Constructive content of proofs . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Higman’s Lemma and Kruskal’s Theorem . . . . . . . . . . . . . . . . . . 3
1.3 Aims and results of the thesis . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Outline of the contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2 Computational Content of Proofs using Inductive Definitions 9
2.1 Extended Heyting Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2 Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Program extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3 Computational Content of Classical Proofs 26
3.1 Refined A-translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.2 Computational content of classical dependent choice . . . . . . . . . . . . 31
3.3 An example for using external realizers . . . . . . . . . . . . . . . . . . . 35
4 Higman’s Lemma and Kruskal’s Theorem 39
4.1 Nash-Williams’ minimal-bad-sequence proof . . . . . . . . . . . . . . . . 39
4.2 Equivalent characterizations of well quasiorderings . . . . . . . . . . . . . 41
4.3 On constructive proofs of Higman’s Lemma and Kruskal’s Theorem . . . 45
5 An inductive version of Nash-Williams’ proof of Higman’s Lemma 49
5.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5.2 The analogy between the classical and the constructive proof . . . . . . . 50
vi