Construction and deduction in type theories [Elektronische Ressource] / Martin Strecker

Martin Strecker

Sujets

• Informatik

Informations

• Publié par: universitat_ulm
• Publié le: 01 janvier 1999
• Nombre de lectures: 21
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Universit¨at Ulm
Abteilung Kunstliche¨ Intelligenz
Leiter: Prof. Dr. Friedrich W. von Henke
Construction and Deduction
in Type Theories
Dissertation zur Erlangung des Doktorgrades Dr. rer. nat.
der Fakult¨at fur¨ Informatik der Universit¨at Ulm
Martin Strecker
aus Darmstadt
1999
()+
+,
!()
!Amtierender Dekan: Prof. Dr. Uwe Sch¨ oning
1. Gutachter: Prof. Dr. Friedrich W. von Henke
2. Gutachter: Prof. Dr. Susanne Biundo-Stephan
ExternerGutachter: Prof. TobiasNipkow,PhD
Tag der Promotion: 28. April 1999Abstract
This dissertation is concerned with interactive proof construction and auto-
mated proof search in type theories, in particular the Calculus of Constructions
and its subsystems.
Typetheoriescanbeconceived asexpressive logicswhichcombineafunc-
tional programming language, strong typing and a higher-order logic. They are
therefore a suitable formalism for specification and verification systems. How-
ever, due to their expressiveness, it is difficult to provide appropriate deductive
support for type theories. This dissertation first examines general methods for
proof construction in type theories and then explores how these methods can
be refined to yield proof search procedures for specialized fragments of the
language.
Proofdevelopment in typetheoriesusually requiresthecontructios n ofa
term having a given type in a given context. For the term to be constructed,
a metavariable is introduced which is successively instantiated in the course
of the proof. A naive use of metavariables leads to problems, such as non-
commutativity of reduction and instantiation and the generation of ill-typed
terms during reduction. For solving these problems, a calculus with explicit
substitutionsisintroduced,anditisshownthatthiscalculuspreservesproper-
ties such as strong normalization and decidability of typing.
In order to obtain a calculus appropriate for proof search, the usual natural
deduction presentation oftype theoriesisreplacedbya sequent style presen-
tation. Itisshown that thecalculusthusobtainediscorrect with respect to
the original calculus. Completeness (proved with a cut-elimination argument)
isshownforallpredicativefragmentsofthelambdacube.
The dissertation concludes with a discussion of some techniques that make
proof search practically applicable, such as unification and pruning of the proof
search space by exploiting impermutabilities of the sequent calculus.Acknowledgements
I want to express my gratitude to Prof. von Henke for supporting throughout
the years the work described in this thesis. I want to thank Prof. Biundo
for accepting to act assecond corrector. I am particularly grateful to Prof.
Nipkow for agreeing spontaneously to join in as external referee.Contents
1. Introduction 1
1.1. Background and Applications ................... 1
1.1.1. The Essence of Type Theory....... 2
1.1.2. Intuitionistic Logic and Type Theory .. 3
1.1.3. Dependent types ...................... 4
1.1.4. Specificationsandmathematicaltheories 5
1.1.5. Proof Assistants.. 8
1.2. Methods ................... 10
1.2.1. “Construction”: Metavariables...... 1
1.2.2. “Deduction”: Proof Search........ 13
1.3. Surveyofthisthesis ........................ 16
1.3.1. Metavariables ... 16
1.3.2. Theory of proof search .......... 20
1.3.3. Pragmaticsofproofsearch ................. 23
2. A Calculus with Metavariables 27
2.1. TheExtendedCalculusofConstructions .... 27
2.1.1. Base calculus – Term language............... 27
2.1.2. Base calculus – Typing .......... 30
2.1.3. Propertiesofthebasecalculus ...... 3
2.1.4. Base calculus – Encodings ................. 36
2.2. Introducing Metavariables ............ 37
2.3. TermcalculuswithMetavariables 39
2.3.1. Metavariables ............ 39
2.3.2. Reduction Relations ........... 42
2.3.3. PropertiesoftheTermCalculus ..... 48
2.4. Proof Problems ........................... 51
2.5. Typing........... 56
2.5.1. Typing: RulesandDefinitions ...... 57
2.5.2. Somepropertiesoftyping ................. 58
2.5.3. Type inference algorithm......... 62
iContents
2.6. SolutionsofMetavariables ..................... 70
2.6.1. Instantiations ...... 70
2.6.2. Verifying instantiations. 78
2.7. Functional Representation of Metavariables............ 81
2.7.1. Definition of the Functional Translation .. 83
2.7.2. StrongNormalizationoftheCalculuswithMetavariables 88
3. A Sequent Calculus Characterization 91
3.1. Natural Deduction and Sequent Systems ............. 91
3.1.1. Survey ..................... 91
3.1.2. Definition of the systems 93
3.2. PropertiesofSequentSystems ........ 97
3.2.1. Correctness ....... 97
3.2.2. Completeness ................. 98
3.3. A Measure for Cut Elimination.......101
3.3.1. The Lambda-Cube ...101
3.3.2. FactsaboutPureTypeSystems .......105
4. Methods of Proof Search 111
4.1. Introduction.............................11
4.2. The Structure of Proofs ....16
4.3. Unification.19
4.3.1. Unification Problems .........19
4.3.2. First-order unification ............121
4.3.3. Higher-order unification128
4.3.4. Unification of Higher-Order “Patterns” ..........13
4.3.5. Discussion ........135
4.4. Tableau-Style Proof Search..............138
4.4.1. SequentCalculusRules ........139
4.4.2. Eigenvariable Conditions146
4.4.3. OptimizationsofProofSearch ........148
5. Conclusions 153
5.1. Summary of Results ........................153
5.2. Evaluation and Perspectives ..154
A. Appendix 157
A.1. A formulation with de Bruijn Indices ...............157
A.1.1. ElementaryconceptsofdeBruijnIndices ..157
A.1.2. TermcalculuswithdeBruijnIndices ....158
A.1.3. Typing with de Bruijn Indices ...............163
iiContents
A.1.4. Definition of instantiations using de Bruijn Indices....163
A.2. Proof of Cut Elimination......................165
A.2.1. Proof........165
A.2.2. Discussion .....174
A.3. ProofsofMiscellaneousTheorems .................175
Bibliography 182
Index 191
iiiList of Figures
2.1. Grammar defining the language of ECC ............. 28
2.2. Rulesofthecalculus ECC .............. 32
2.3. Codingoflogicalconnectivesin ECC ........ 36
2.4. Grammar defining the language of ECC with metavariables .. 40
2.5. TypingrulesforMetavariables ........ 57
3.1. Rulesofthecalculus ECC ............. 94
G
3.2. The Lambda Cube ..............102
3.3. Typing rules for the systems of the Lambda Cube .103
3.4. Sort combinations for the systems of the Lambda Cube .....104
4.1. First-order unification .......................123
4.2. First-order cumulative unification ..........125
4.3. Lift rule .............131
4.4. RulesoftheTableaucalculus ........141
4.5. Solutions associated with the Tableau rules.....142
4.6. Proofelementsoflogicalconnectivesandquantifiers143
4.7. Rules of Proof Transformation System ..............14
A.1. Grammar defining the language with de Bruijn Indices .....158
A.2. TypingrulesusingdeBruijnIndices ...............162
A.3. TypingrulesforMetavariablesusingdeBruijnIndices .....163
iv1. Introduction
1.1. Background and Applications
Specification and verification isbecoming an increainglys important activity
accompanying the design and development of complex systems. Formal spec-
ification and verification, in particular, permit to attain a degree of precision
that cannot be achieved with informal methods. A more widespread use of
formal techniques is however often hampered by a lack of expressiveness of
specification languages or by insufficient deductive capabilities of verification
environments.
Someadvancedtypetheoriesarepromisingcandidatesforspecificationfor-
malisms, since they combine computational aspects, strong typing and a higher-
order logic within one homogeneous framework. Moreover, essential concepts
such as module, parameterization, refinement and realization of a specification
can be internalized in type theory and thusdo not require an extra-logical
treatment.
Thisthesiscontributesto thetudys of deductiveupps ort for type theo-
ries. In order to take advantage of the full expressiveness of the type theoretic
languages under consideration, the investigation starts from a rather broad
perspective. Since fully automated proof procedures can realistically only be
formulated for limited language fragments, appropriate restrictions have to be
imposed in the sequel. Thus, as suggested by the title, this thesis is concerned
with
• constructionofentitiesofthefulllanguageinawaywhichissound(in
that it respects typing) and consistent (in that it is in accordance with
evaluation of programs).
• deduction in a more traditional sense, which however is smoothly inte-
grated with the “constructive” aspect and which makes essential use of
techniquesdevelopedinthemoregeneralsetting.
In the following, we will informally present some key concepts of type the-
ories(Sections 1.1.1 to 1.1.4) and proof assistants based on type theory (Sec-
11.1. BACKGROUND AND APPLICATIONS
tion 1.1.5), with the purpose of exposing some problems that have to be faced
when trying to develop an appropriate deductive machinery for a specification
and verification environment. In Section 1.2, we will exemplify some of the
solutions that are proposed in this thesis to ach