Decidability for non-standard conversions in typed lambda-calculi [Elektronische Ressource] / Freiric Barral

Freiric Barral

Sujets

• Informatik

Informations

• Publié par: ludwig-maximilians-universitat_munchen
• Publié le: 01 janvier 2008
• Nombre de lectures: 16

Extrait

These de doctorat de l’universite de Toulouse III - Paul Sabatier
Institut de Recherche en Informatique de Toulouse
Ecole Doctorale Mathematiques, Informatique et Telecommunications de Toulouse.
Specialite informatique
Dirigee en cotutelle / Ko-Betreuung
Dissertation an der Fakultat fur Mathematik, Informatik und Statistik der
Ludwig-Maximilian-Universitat Munchen.
Decidability for Non-Standard Conversions
in Typed Lambda-Calculi
Freiric Barral
These pour obtenir le grade de docteur d’universite.
Dissertation zur Erlangung des Grades eines Doktors der
Naturwissenschaften.
Supervisors:
Prof. Dr. Martin Hofmann
Prof. Dr. Serge Soloviev
First external reviewer: Prof. Dr. Olivier Danvy
Second external reviewer: Prof. Dr. Pierre Damphousse
First examiner: Prof. Dr. Rolf Hennicker
Second examiner: Prof. Dr. Hans Jurgen Ohlbach
Date of the oral examination: 6 June 2008
Munich, April 2008Decidability for Non-Standard Conversions
in Typed Lambda-CalculiThese de doctorat de l’universite de Toulouse III - Paul Sabatier
Institut de Recherche en Informatique de Toulouse
Ecole Doctorale Mathematiques, Informatique et Telecommunications de Toulouse.
Specialite informatique
Dirigee en cotutelle / Ko-Betreuung
Dissertation an der Fakultat fur Mathematik, Informatik und Statistik der
Ludwig-Maximilian-Universitat Munchen.
Decidability for Non-Standard Conversions
in Typed Lambda-Calculi
Freiric Barral
These pour obtenir le grade de docteur d’universite.
Dissertation zur Erlangung des Grades eines Doktors der
Naturwissenschaften.
Supervisors:
Prof. Dr. Martin Hofmann
Prof. Dr. Serge Soloviev
First external reviewer: Prof. Dr. Olivier Danvy
Second external reviewer: Prof. Dr. Pierre Damphousse
First examiner: Prof. Dr. Rolf Hennicker
Second examiner: Prof. Dr. Hans Jurgen Ohlbach
Date of the oral examination: 6 June 2008
Munich, April 2008Contents
Acknowledgements 1
Introduction 3
1 Preliminaries 11
1.1 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2 Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2 Simply Typed -Calculus 15
2.1 System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2 Normalization by Evaluation . . . . . . . . . . . . . . . . . . . . . . . 19
2.2.1 Informal Description . . . . . . . . . . . . . . . . . . . . . . . 19
2.2.2 Normal Forms . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.3 Name Generation Environment . . . . . . . . . . . . . . . . . 25
2.3 Formalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.3.1 Name Generation Interpretation . . . . . . . . . . . . . . . . . 28
2.3.2 Monadic logical relation . . . . . . . . . . . . . . . . . . . . . 35
2.3.3 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
2.3.4 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
Conversions . . . . . . . . . . . . . . . . . . . . . . . . . . 51
Completeness Lemma . . . . . . . . . . . . . . . . . . . . . . . 54
3 Generalized Applications 57
3.1 From Sequent Calculus to . . . . . . . . . . . . . . . . . . . . . . 58J
3.2 Extended Conversions and Normal Forms . . . . . . . . . . . . . . . . 60
3.3 Informal Description . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
3.3.1 Several Attempts . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.3.2 The Binding Variable Problem . . . . . . . . . . . . . . . . . . 68
3.4 Formalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
4 Sums 75
4.1 System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
4.2 Extended Conversion and Normal Forms . . . . . . . . . . . . . . . . 80vi Contents
4.3 Informal Description . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
4.3.1 Several Attempts . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.3.2 The Binding Variable Problem . . . . . . . . . . . . . . . . . . 87
4.3.3 Toward Completeness . . . . . . . . . . . . . . . . . . . . . . . 89
4.3.4 Normal Forms . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
4.4 Formalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
5 Inductive Types 99
5.1 System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
5.1.1 Types and Schemas . . . . . . . . . . . . . . . . . . . . . . . . 100
5.1.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.1.3 Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
5.2 Extended Conversions . . . . . . . . . . . . . . . . . . . . . . . . . . 106
5.2.1 General Results . . . . . . . . . . . . . . . . . . . . . . . . . . 106
5.2.2 Inductive Type Schemas as Functors . . . . . . . . . . . . . . 107
5.3 Main Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5.3.1 Adjournment . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5.3.2 Convergence of . . . . . . . . . . . . . . . . . . . . . . 1102
5.3.3 Pre-adjusted Adjournment . . . . . . . . . . . . . . . . . . . . 112
5.3.4 Convergence of