On extensions of AF2 with monotone and clausular (Co)inductive definitions [Elektronische Ressource] / vorgelegt von Favio Ezequiel Miranda Perea

Miranda-Perea, Favio

Sujets

• Informatik
• Mathematics

Informations

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

Extrait

On Extensions of AF2 with Monotone and
Clausular (Co)inductive De nitions
Dissertation
zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften an der Fakultat fur
Mathematik, Informatik und Statistik der
Ludwig-Maximilians-Universitat Munchen
vorgelegt von
Favio Ezequiel Miranda Perea
aus Mexiko-Stadt
im September 20041. Berichterstatter: Prof. Dr. Helmut Schwichtenberg
2. Berich Prof. Dr. Wilfried Buchholz
Tag des Rigorosums: 12. November 2004Contents
Abstract vii
Zusammenfassung ix
Acknowledgements xi
Agradecimientos xiii
Introduction xv
1 Preliminaries 1
1.1 Categorical Interlude . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1.1 M-(Co)algebras . . . . . . . . . . . . . . . . . . . . . . . . 5
1.1.2 Dialgebras . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2 The Type System F . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2.1 Adding Sum and Product Types . . . . . . . . . . . . . . 14
1.2.2 Adding Existential Types . . . . . . . . . . . . . . . . . . 22
1.2.3 On Embeddings . . . . . . . . . . . . . . . . . . . . . . . 23
1.3 Second Order Logic AF2 . . . . . . . . . . . . . . . . . . . . . . . 24
1.3.1 De nition of the System . . . . . . . . . . . . . . . . . . . 24
1.3.2 Strong Normalization of AF2 . . . . . . . . . . . . . . . . 29
1.3.3 Adding Conjunctions and Disjunctions . . . . . . . . . . . 29
2 Extensions of System F with Monotone (Co)inductive Types 31
2.1 From Categories to Types . . . . . . . . . . . . . . . . . . . . . . 31
2.1.1 Representing (Co)algebras . . . . . . . . . . . . . . . . . . 32
2.1.2ting Dialgebras . . . . . . . . . . . . . . . . . . . 35
2.2 The System MICT . . . . . . . . . . . . . . . . . . . . . . . . . . 37
2.2.1 De nition of the System . . . . . . . . . . . . . . . . . . . 37
2.2.2 Strong Normalization of MICT . . . . . . . . . . . . . . . 39
2.3 The System MCICT . . . . . . . . . . . . . . . . . . . . . . . . . 52
2.3.1 De nition of the System . . . . . . . . . . . . . . . . . . . 52
2.3.2 Strong Normalization of MCICT . . . . . . . . . . . . . . 57
2.3.3 On -rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
2.3.4 Canonical Monotonicity Witnesses . . . . . . . . . . . . . 65
2.3.5 (Co)recursive Programming in MCICT . . . . . . . . . . . 68
2.4 The System MCICT . . . . . . . . . . . . . . . . . . . . . . . . 75M
iiiiv CONTENTS
2.4.1 De nition of the System . . . . . . . . . . . . . . . . . . . 75
2.4.2 Strong Normalization of MCICT . . . . . . . . . . . . . 76M
2.5 The Hybrid System MCICT . . . . . . . . . . . . . . . . . . 77 M
3 Monotone and Clausular (Co)inductive De nitions 79
3.1 Fixed-Point Theory . . . . . . . . . . . . . . . . . . . . . . . . . . 79
3.2 The Logic MCICD . . . . . . . . . . . . . . . . . . . . . . . . . . 80
3.3 Strong Normalization of MCICD . . . . . . . . . . . . . . . . . . . 86
3.4 Canonical Monotonicity Witnesses . . . . . . . . . . . . . . . . . 87
4 Realizability for MCICD 93
?
4.1 The Logic MCICD . . . . . . . . . . . . . . . . . . . . . . . . . . 93
4.1.1 De nition of the Logic . . . . . . . . . . . . . . . . . . . . 93
?
4.1.2 Strong Normalization of MCICD . . . . . . . . . . . . . . 95
?4.1.3 Subject Reduction for MCICD . . . . . . . . . . . . . . . 95
4.2 The Realizability Interpretation . . . . . . . . . . . . . . . . . . . 104
4.2.1 Realizing the Axioms . . . . . . . . . . . . . . . . . . . . 106
4.2.2 The Soundness Theorem . . . . . . . . . . . . . . . . . . . 120
5 Programming with Proofs 127
5.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
5.1.1 Syntactical Models for the Term System . . . . . . . . . . 127
?
5.1.2 Semantics for the Logic MCICD . . . . . . . . . . . . . . 132
5.2 Formal Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . 142
5.2.1 A Connection with Modi ed Realizability . . . . . . . . . 143
5.2.2 The Canonical Model . . . . . . . . . . . . . . . . . . . . 144
5.2.3 Examples of Data Types . . . . . . . . . . . . . . . . . . . 145
5.3 Programming with Proofs in MCICD . . . . . . . . . . . . . . . . 150
5.3.1 Programming Functions with Iteration or Recursion . . . 151
5.3.2 F with Coiteration or Corecursion . 156
6 A System with Mendler-style Coinduction 159
6.1 Fixed-Point Theory . . . . . . . . . . . . . . . . . . . . . . . . . . 159
6.2 The Logic MCICD . . . . . . . . . . . . . . . . . . . . . . . . 160 M
6.3 Realizability for MCICD . . . . . . . . . . . . . . . . . . . . 162 M
6.3.1 Realizing the Axioms . . . . . . . . . . . . . . . . . . . . 162
6.3.2 The Soundness Theorem . . . . . . . . . . . . . . . . . . . 164
6.4 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
6.5 Programming with Proofs in MCICD . . . . . . . . . . . . . 169 M
6.5.1 Data types with Equality . . . . . . . . . . . . . . . . . . 170
6.5.2 Programming with Mendler-style Coiteration or Corecur-
sion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175CONTENTS v
7 Conclusions and Future Work 179
7.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179
7.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
7.3 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182
Bibliography 187
Symbol Index 193
Index 195
Lebenslauf 199vi CONTENTSAbstract
This thesis discusses some extensions of second-order logic (AF2) with primitive
constructors representing leastand greatest xed points of monotone operators,
which allow to de ne predicates by induction and coinduction. Though the ex-
pressive power of second-order logic has been well-known for a long time and
su ces to de ne (co)inductive predicates by means of its (co)induction princi-
ples, it is more user-friendly to have a direct way of de ning predicates induc-
tively. Moreover recent applications in computer science oblige to consider also
coinductive de nitions useful for handling in nite objects, the most prominent
example being the data type of streams or in nite lists. Main features of our
approach are the use clauses in the (co)inductive de nition mechanism, concept
which simpli es the syntactic shape of the predicates, as well as the inclusion
of not only (co)iteration but also primitive (co)recursion principles and in the
case of coinductive de nitions an inversion principle. For sake of generality we
consider full monotone, and not only positive de nitions |after all positivity is
only used to ensure monotonicity.
Working towards practical use of our systems we give them realizability inter-
pretations where the systems of realizers are strongly normalizing extensions of
the second-order polymorphic lambda calculus, system F, in Curry-style, with
(co)inductive types corresponding directly to the logical systems via the Curry-
Howard correspondence. Such realizability interpretations are therefore not
reductive: the de nition of realizability for a (co)inductive de nition is again a
(co)inductive de nition. As main application of realizability we extend the so-
called programming-with-proofs paradigm of Krivine and Parigot to our logics,
by means of which a correct program of the lambda calculus can be extracted
from a proof in the logic.
viiviii 0. ABSTRACTZusammenfassung
Diese Dissertation besch aftigt sich mit Erweiterungen der Logik zweiter Stufe
(AF2) mit primitiven Konstruktoren, die kleinste und gr o te Fixpunkte mono-
toner Operatoren repr asentieren, mit denen Pr adikate durch Induktion und
Koinduktion lassen sich de nieren. Obwohl die Ausdrucksf ahigkeiten der zweit-
stu ger Logik schon seit lange Zeit bekannt sind und reichen um (ko)induktive
Pr adikate, mittels ihre (ko)induktion Prinzipien zu de nieren, es ist freundlicher,
eine direkte Weise zu haben, Pr adikate induktiv zu de nieren. Darub er hin-
aus fordern letzte Anwendungen in der Informatik koinduktive De nitionen
zu betrachten, welche nutzlic h fur die Behandlung unendlicher Objekte sind,
das bedeutendste Beispiel sei die Datentyp von Str ome oder unendliche Lis-
ten. Hauptbeitr age unsere Behandlung sind der Gebrauch von Klauseln in dem
Mechanismus (ko)induktiver De nierung. Konzept, das die syntaktische Form
der Pr adikate vereinfacht, sowie die Betrachtung nicht nur von (Ko)iteration
sondern auch von Prinzipien primitiver (Ko)rekursion. Im Interesse der All-
gemeinheit, betrachten wir voll monoton, und nicht nur positive De nitionen,
immerhin die syntaktische Beschr ankung zu positiven De nitionen ist nur ver-
wendet, um Monotonie sicherzustellen.
In Richtung praktischer Anwendungen unserer Systemen geben wir ihnen Re-
alisierbarkeitsinterpretationen, wobei die Systeme von Realisierern stark nor-
malisierende Erweiterungen des polymorphen Lambda Kalkuls zweiter Stufe,
System F a la Curry, mit (ko)induktive Typen sind, die direkt den logischen
Systemen durch die Curry-Howard Korrespondenz entsprechen. Solche Real-
isierbarkeitsinterpretationen sind folglich nicht reduktive: die De nition der
Realisierbarkeit fur eine (ko)induktive De nition ist wieder eine (ko)induktive
De nition. Als Hauptanwendung der Realisierbarkeit werde das sogenannte
programmieren-mit-Beweise Verfahren von Krivine und Parigot auf unsere Logik
erweitert, mit welchem ein korrektes Programm des Lambda-Kalkuls aus einem
Beweis in der Logi