La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

these

148 pages
oN d’ordre: 000`THESE DE DOCTORAT DE´L’UNIVERSITE PARIS 6Sp´ecialit´eInformatiquepr´esent´ee parEmmanuel Coquerypour obtenir le grade de´Docteur de l’universite de Paris 6´Ecole doctorale : Informatique, T´el´ecommunications et Electronique de ParisUFR D’INFORMATIQUELaboratoire : INRIA-Rocquencourt´Equipe d’accueil : ContraintesTitre de la th`ese :Typage et programmation en logique avec contraintesSoutenue le 3 D´ecembre 2004 devant le jury compos´e de :Me. : Ir`ene Guessarian Pr´esidenteMM. : Jean Goubault-Larrecq RapporteursJan MaluszynskiFranc¸ois PottierMe. : V´eronique Donzeau-Gouge ExaminatriceM. : Franc¸ois Fages DirecteurR´esum´eLes langages logiques avec contraintes sont des langages non typ´es. Les pro-grammeurs qui utilisent ces langages b´en´eficient donc d’une grande souplesse deprogrammation, au d´etriment des avantages apport´es par le typage, en particulierla d´etection d’erreurs de programmation.Cette th`ese d´ecrit un syst`eme de types pour les langages logiques avec con-traintes, de sa formalisation `a sa mise en œuvre. Ce syst`eme combine poly-morphisme param´etrique, sous-typage et surcharge pour obtenir la souplessen´ecessaire au typage de programmes utilisant des techniques de programmationlogique avec contraintes comme la m´eta-programmation et l’utilisation conjointede diff´erents domaines de contraintes. Le syst`eme est prouv´e coh´erent par rap-port `a la r´esolution CSLD et par rapport `a un mod`ele d’ex´ecution ...
Voir plus Voir moins

oN d’ordre: 000
`THESE DE DOCTORAT DE
´L’UNIVERSITE PARIS 6
Sp´ecialit´e
Informatique
pr´esent´ee par
Emmanuel Coquery
pour obtenir le grade de
´Docteur de l’universite de Paris 6
´Ecole doctorale : Informatique, T´el´ecommunications et Electronique de Paris
UFR D’INFORMATIQUE
Laboratoire : INRIA-Rocquencourt
´Equipe d’accueil : Contraintes
Titre de la th`ese :
Typage et programmation en logique avec contraintes
Soutenue le 3 D´ecembre 2004 devant le jury compos´e de :
Me. : Ir`ene Guessarian Pr´esidente
MM. : Jean Goubault-Larrecq Rapporteurs
Jan Maluszynski
Franc¸ois Pottier
Me. : V´eronique Donzeau-Gouge Examinatrice
M. : Franc¸ois Fages DirecteurR´esum´e
Les langages logiques avec contraintes sont des langages non typ´es. Les pro-
grammeurs qui utilisent ces langages b´en´eficient donc d’une grande souplesse de
programmation, au d´etriment des avantages apport´es par le typage, en particulier
la d´etection d’erreurs de programmation.
Cette th`ese d´ecrit un syst`eme de types pour les langages logiques avec con-
traintes, de sa formalisation `a sa mise en œuvre. Ce syst`eme combine poly-
morphisme param´etrique, sous-typage et surcharge pour obtenir la souplesse
n´ecessaire au typage de programmes utilisant des techniques de programmation
logique avec contraintes comme la m´eta-programmation et l’utilisation conjointe
de diff´erents domaines de contraintes. Le syst`eme est prouv´e coh´erent par rap-
port `a la r´esolution CSLD et par rapport `a un mod`ele d’ex´ecution typ´e avec
substitutions. Un algorithme de v´erification des types avec inf´erence du type des
variables et gestion efficace de la surcharge a ´egalement ´et´e d´evelopp´e, ainsi qu’un
algorithme heuristique d’inf´erence de type pour les pr´edicats.
Cette th`ese s’int´eresse ´egalement au probl`eme de la satisfiabilit´e des contraintes
d’ordre dans les quasi-treillis, qui constituent des structures de types riches,
ajoutant ainsi de la souplesse au syst`eme de type. Le probl`eme de satisfiabi-
lit´e est montr´e NP-complet dans le cas de quasi-treillis dont les extrema sont
3des constantes en nombre fini. La complexit´e de l’algorithme devient O(n ) dans
le cas ou` toutes les variables du syst`eme de contraintes sont born´ees. Un algo-
rithme pour le calcul explicite de solutions est ´egalement pr´esent´e. De plus, cet
algorithme permet de tester la satisfiabilit´e dans des quasi-treillis dont seuls les
maxima sont des constantes en nombre fini. Ces r´esultats sur les quasi-treillis sont
g´en´eraux et leur port´ee n’est pas limit´ee au typage.
Mots cl´e : Typage, Sous-typage, Polymorphisme param´etrique, Surcharge,
Contraintes de sous-typage, Programmation logique avec contraintes.Abstract
Constraint logic languages are untyped. The programmers that use these lan-
guages therefore benefit from a high flexibilty in programming, to the detriment
of the advantages of typing, in particular the detection of programming errors.
This thesis describes a type system for constraint logic languages, from its
formalization to its implementation. This system combines parametric polymor-
phism with subtyping and overloading to obtain the flexibility that is needed for
typing programs using logic programming techniques such as metaprogramming
and the simultaneous use of different constraint domains. The system is proven
coonsistent with reference to the CSLD resolution and with reference to a typed
execution model with substitutions. An type checking algorithm, with type infe-
rence for variables and an efficient management of overloading was developped,
as well as a heuristic algorithm for infering the type of predicates.
This thesis also addresses the problem of the satisfiability of ordering constraints
in quasi-lattices, which are rich type structures, thus adding more flexibility to
the type system. The problem of satisfiability is proven NP-complete for the case
of quasi-lattices where the set of extrema is finite and contains only constants.
3The complexity of this algorithm becomes O(n ) when all the variables in the
constraint system are bounded. An algorithm for computing explicit solutions
is also presented. Moreover, this algorithm allows for testing the satisfiability in
quasi-lattices where only the maxima are constants and in finite number. These
results on quasi-lattices are general and are not limited to typing.
Keywords : Typing, Subtyping, Parametric polymorphism, Overloading,
Subtyping constraints, Constraint logic programming.Remerciements
Je tiens tout particuli`erement `a remercier Franc¸ois Fages pour m’avoir guid´e
et soutenu durant toute la dur´ee de ma th`ese. Ses nombreux conseils, tant sur
le plan purement scientifique que sur la d´emarche d’un chercheur m’ont ´et´e tr`es
pr´ecieux.
Jean Goubault-Larrecq, Franc¸ois Pottier et Jan Ma luszyn´ski ont accept´e la
lourde tˆache de rapporteur. Je les remercie chaleureusement pour le temps et
l’int´erˆet qu’ils ont port´e `a mon travail.
Je remercie ´egalement V´eronique Donzeau-Gouge et Ir`ene Guessarian qui ont
bien voulu faire partie de ce jury.
Je tiens ´egalement `a remercier les membres du projet Contraintes au sein
duquel j’ai effectu´e cette th`ese, pour leur bonne humeur quotidienne.
Je remercie tous les membres de ma famille et tous mes amis pour leur soutien
et leurs encouragements sans faille.
Enfin, je remercie ma femme, Sandrine-Dominique Gouraud, pour son amour,
son soutien ind´efectible et la patience dont elle a fait preuve `a mon ´egard. Elle a
´et´e pour moi une extraordinaire source d’inspiration et de courage.Table des mati`eres
1 Introduction 13
2 Pr´eliminaires CLP 23
2.1 Programmes CLP(X ) . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.1 Contraintes . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.2 Programmes . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.2 R´esolution CSLD . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3 Le langage CHR . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
I Contraintes de sous-typage dans les quasi-treillis 31
3 Langage de types 33
3.1 Introduction au sous-typage . . . . . . . . . . . . . . . . . . . . . 33
´3.2 Etiquettes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.4 Ordre sur les types . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.5 Contraintes de sous-typage . . . . . . . . . . . . . . . . . . . . . . 39
4 Quasi-treillis de types 43
4.1 Pr´eliminaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.2 Constructeurs de types . . . . . . . . . . . . . . . . . . . . . . . . 45
4.3 Construction de bornes pour les types infinis . . . . . . . . . . . . 47
4.4 Preuve du th´eor`eme . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.5 Types r´eguliers et types finis . . . . . . . . . . . . . . . . . . . . . 54
5 Syst`emes de contraintes clos 57
5.1 D´efinitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.2 Satisfiabilit´e des syst`emes clos . . . . . . . . . . . . . . . . . . . . 58
5.3 Algorithmes de clˆoture . . . . . . . . . . . . . . . . . . . . . . . . 64
9`10 TABLE DES MATIERES
6 Calcul de bornes 69
6.1 Syst`eme de r´e´ecriture pour le calcul de bornes . . . . . . . . . . . 70
6.2 Propri´et´es du syst`eme de r´e´ecriture . . . . . . . . . . . . . . . . . 74
6.2.1 Terminaison . . . . . . . . . . . . . . . . . . . . . . . . . . 74
6.2.2 Correction . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
6.2.3 Satisfiabilit´e d’un syst`eme de contraintes . . . . . . . . . . 81
6.2.4 Solutions explicites optimales . . . . . . . . . . . . . . . . 84
6.2.5 Ind´ependance vis-`a-vis du choix des r`egles . . . . . . . . . 85
6.3 Algorithme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
6.4 Implantation en CHR . . . . . . . . . . . . . . . . . . . . . . . . . 87
6.4.1 Structures de donn´ees . . . . . . . . . . . . . . . . . . . . 88
6.4.2 Strat´egie utilis´ee . . . . . . . . . . . . . . . . . . . . . . . 89
6.4.3 Mise `a jour des contraintes . . . . . . . . . . . . . . . . . . 89
6.4.4 Unification de variables de types . . . . . . . . . . . . . . . 90
6.4.5 Performances . . . . . . . . . . . . . . . . . . . . . . . . . 91
II Typage des langages logiques avec contraintes 95
7 Syst`eme de types 97
7.1 Programmes bien typ´es . . . . . . . . . . . . . . . . . . . . . . . . 97
7.1.1 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
7.1.2 R`egles de typage . . . . . . . . . . . . . . . . . . . . . . . 98
7.2 Coh´erence au mod`ele d’ex´ecution CSLD . . . . . . . . . . . . . . 101
7.3 Coh´erence au mod`ele avec substitutions . . . . . . . . . . . . . . . 101
7.3.1 Mod`ele d’ex´ecution typ´e . . . . . . . . . . . . . . . . . . . 103
7.4 Choix des types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
7.4.1 M´eta-programmation . . . . . . . . . . . . . . . . . . . . . 105
7.4.2 Surcharge et sous-typage . . . . . . . . . . . . . . . . . . . 106
7.4.3 Expressions arithm´etiques . . . . . . . . . . . . . . . . . . 107
7.4.4 Structures pour diff´erents syst`emes . . . . . . . . . . . . . 107
8 V´erification des types 111
8.1 Syst`eme de type dirig´e par la syntaxe . . . . . . . . . . . . . . . . 111
8.2 Algorithme de v´erification des types . . . . . . . . . . . . . . . . . 114
8.2.1 Inf´erence de types pour les variables . . . . . . . . . . . . 114
8.2.2 Gestion de la surcharge . . . . . . . . . . . . . . . . . . . . 115
8.2.3 Description de l’algorithme . . . . . . . . . . . . . . . . . . 115
8.2.4 Implantation en CHR . . . . . . . . . . . . . . . . . . . . . 116
8.3 R´esultats exp´erimentaux . . . . . . . . . . . . . . . . . . . . . . . 117
8.3.1 D´etection d’erreurs de programmation . . . . . . . . . . . 117