Du typage vectoriel, On vectorial typing

Alejandro Diaz Caro

Description

Sous la direction de Pablo Arrighi
Thèse soutenue le 23 septembre 2011: Grenoble
L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.
-Theorie des types
-Lambda calcul algébrique
-Informatique quantique
The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.
-Type theory
-Algebraic lambda calculus
-Quantum computing
Source: http://www.theses.fr/2011GRENM038/document

Sujets

• Théorie des types
• Informatique quantique

Informations

• Publié par: Thesee
• Nombre de lectures: 80
• Langue: Français
• Poids de l'ouvrage: 2 Mo

Extrait

THÈSE
Pour obtenir le grade de
DOCTEURDEL’UNIVERSITÉDEGRENOBLE
Spécialité : Informatique
Arrêté ministériel:7 août2006
Présentée par
AlejandroDÍAZ-CARO
Thèsedirigée parPabloARRIGHI
et codirigée parFrédéricPROST
préparée au sein duLaboratoired’InformatiquedeGrenoble
et de l’École Doctorale Mathématiques, Sciences et Technologies de
l’Information, Informatique
Dutypagevectoriel
Thèsesoutenue publiquementle23Septembre2011,
devantle jury composéde :
M.PhilippeJORRAND
Directeur de Recherche Émérite CNRS, HDR, Président
M.EduardoBONELLI
Profesor Asociado à l’UNQ et Investigador Adjunto au CONICET,Rapporteur
M.GillesDOWEK
Directeur de Recherche INRIA, HDR, Rapporteur
M.ThomasEHRHARD
Directeur de Recherche CNRS, HDR, Rapporteur
M.MichelePAGANI
Maître de Conférences à l’Université de Paris Nord, Examinateur
M.LaurentREGNIER
Professeurà l’Université de la Méditerranée, HDR, Examinateur
M.LionelVAUX
Maître de Conférences à l’Université de la Méditerranée, Examinateur
M.PabloARRIGHI
Maître de Conférences à l’Université de Grenoble, HDR, Directeur de thèse
tel-00631514, version 1 - 12 Oct 2011tel-00631514, version 1 - 12 Oct 2011a Nache
mi compañera de ruta
tel-00631514, version 1 - 12 Oct 2011tel-00631514, version 1 - 12 Oct 2011i
Résumé
’objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique,
une extensionduλ-calculmotivéparl’informatiquequantique. CetteextensionalgébriquecomprendL touslestermesduλ-calculplusleurscombinaisonslinéaires,doncsitetrsontdestermes,α.t+β.r
est aussi un terme, avec α et β des scalaires pris dans un anneau. L’idée principale et le défi de cette
thèse était d’introduire un système de types où les types, de la même façon que les termes, constituent un
espace vectoriel, permettant la mise en évidence de la structure de la forme normale d’un terme. Cette
thèse présente le système Lineal, ainsi que trois systèmes intermédiaires, également intéressants en eux-
CAmême : Scalar, Additive et λ , chacun avec leurs preuves de préservation de type et de normalisation
forte.
Abstract
heobjectiveofthisthesisistodevelopatypetheoryforthelinear-algebraicλ-calculus,anextension
ofλ-calculus motivated by quantum computing. This algebraic extension encompasses all the termsTofλ-calculus together with their linear combinations, so ift andr are two terms, so isα.t+β.r, with
α andβ being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type
system where the types, in the same way as the terms, form a vectorial space, providing the information
about the structure of the normal form of the terms. This thesis presents the system Lineal, and also
CAthree intermediate systems, however interesting by themselves: Scalar, Additive and λ , all of them
with their subject reduction and strong normalisation proofs.
tel-00631514, version 1 - 12 Oct 2011ii
tel-00631514, version 1 - 12 Oct 2011iii
Acknowledgements
This thesis would not have been possible without the guidance and help of several individuals, who
in one way or another have contributed and extended their valuable assistance in the preparation and
completion of this study.
First, my utmost gratitude to Pablo Arrighi, my adviser, who trusted me from the beginning. He
encouraged me at every step, not only in scientific matters but also for my integration in France. His
motivation, enthusiasm and foremost, his confidence in me, are what made me always try harder.
I thank Frédéric Prost for sharing the task of co-advising this thesis.
The INS2I-PEPS project QuAND has financed me several times to go abroad and present the result
of these works, for which I want to thank its coordinator Lionel Vaux. This work was also partially
surpported by the ANR-JCJC project CausaQ and the European FP6-STREP project QICS.
Iwanttothank toChristine Tasson,withwhomIhavehadthe pleasuretowork. Ialsothank Barbara
Petit, who has been a source of brilliant ideas, and who has become a very good friend. My thanks also
go to Benoît Valiron and Simon Perdrix, with whom I have had the privilege of working and sharing
experiences; it has been always fruitful to work with them.
I extend my gratitude to my masters student, Pablo Buiras,and his co-adviser,Mauro Jaskelioff,with
whom I have spent hours discussing via skype and email, which enriched me every time.
IamverygratefulwithEduardoBonelli,GillesDowek,LaurentRegnier,LionelVaux,MichelePagani,
Philippe Jorrand and Thomas Ehrhard for giving me the honour of evaluating this thesis and for their
useful comments and enlightening discussions.
I am grateful to my fellow labmates, Jonathan Grattage, Renan Fargetton, Simon Perdrix and Mehdi
Mhalla, for the stimulating discussions and for all the fun we have had over the last three years. In
particular, I want to especially thank Jon and his wife Janine for their invaluable friendship, and for all
the proofreading they have done over the past three years; and Simon for all his encouragement, and for
being the first to make me learn French with his infinite patience. I also thank the whole CAPP team
for having received me within the group.
The lack of typos and the improved English in this thesis are due to Barbara, Brian, Endo, Gabriela,
Isolda, Janine, Jon, Rodrigo and Santi. Thanks! On the other hand, the enormous amount of typos and
bad English that are still here, are my fault entirely.
I cannot forget to thank to all the Ñ mailing list, my source of great amusement at a distance.
I want to express a special thanks to my mother, who has alwayssupported me and encouragedme to
followmydreams. She alwaysinstilledmethe loveforknowledge,fromanearlyage,whensheencouraged
me when I participated in the school science club, and bought me every book I asked for to satisfy my
growing curiosity during my childhood.
To my brothers andsistersFélix, Diego, Mariano,Paty, Sol, Belén andEstefy, my brothersandsisters
in law, my nephews and nieces, my uncles and aunts: thanks for always being there, for support me and
for that much love.
Most importantly, I want to thank my wife Nache, who has given me her support, understanding and
love, and was on my side during all the successes and failures over the past three years, and before. It
would not have been possible to finish this thesis without her. To her I dedicate this thesis.
tel-00631514, version 1 - 12 Oct 2011iv
tel-00631514, version 1 - 12 Oct 2011Contents
1 Introduction 1
1.1 A brief and fast introduction to the quantum notation . . . . . . . . . . . . . . . . . . . . 3
1.2 The linear-algebraicλ-calculus (λ ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5lin
1.2.1 Some technical remarks aboutλ . . . . . . . . . . . . . . . . . . . . . . . . . . . 6lin
1.2.2 Encoding quantum computation in λ . . . . . . . . . . . . . . . . . . . . . . . . 7lin
1.3 Plan of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2 Call-by-name, call-by-base and the reduction/equality duality 11
2.1 Algebraicλ-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Discussion on consistency and confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2.1 Local confluence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2.2 Simulations and the confluence issue . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.3 Simulations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.1 Algebraic reduction versus algebraic equality . . . . . . . . . . . . . . . . . . . . . 18
2.3.2 Call-by-name simulates call-by-base . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.3.3 Call-by-base simulates call-by-name . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3.4 The remaining simulations. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.4 Conclusion and open questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3 A type system accounting for scalars 27
3.1 The Scalar Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.2 Subject reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.1 Preliminary lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.2.2 Subject reduction proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.3 Strong normalisation, simplified reduction rules and confluence . . . . . . . . . . . . . . . 35
3.4 Barycentricλ-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.5 Conclusion and open questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4 Introducing sums of types 43
add4.1 The Additive Type System for λ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.2 Subject reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.3 Logic