Confluence properties of rewrite rules by decreasing diagrams

Résumé : Cette thèse étudie la confluence des systèmes de récriture en l'absence de propriété de terminaison, pour des applications aux langages fonctionnels de premier ordre comme MAUDE, ou aux langages d'ordre supérieur comportant des types dépendants, comme Dedukti. Dans le premier cas, les calculs opérant sur des structures de données infinies ne terminent pas. Dans le second, les calculs non typés ne terminent pas à cause de la beta-réduction. Dans le cas où les calculs terminent, la confluence se réduit à celle des pics critiques, divergences minimales du calcul, obtenues à partir d'un terme médian appellé superposition qui se récrit de deux manière différentes en une paire de termes appellée critique. Dans le cas où les calculs ne terminent pas, le résultat majeur est que les calculs définis par des règles linéaires à gauche et sans paires critiques confluent. Il s'agit donc d'étendre ce résultat aux systèmes dont les règles peuvent être non-linéaires à gauche et avoir des paires critiques.L'étude la confluence est faite à partir de la méthode des diagrammes décroissants, qui généralise les techniques utilisées antérieurement aussi bien pour des calculs qui terminent que pour des calculs qui ne terminent pas. Cette technique est abstraite, en ce sens qu'elle s'applique à des relations arbitraires opérant sur un ensemble abstrait. Elle consiste à équipper chaque étape de calcul d'un label pris dans un ensemble bien fondé. Un pic de calcul, composé d'un terme se récrivant de deux manières différentes, possède un diagramme décroissant lorsque ses extémités peuvent se récrire en un terme commun avec des étapes de calcul satisfaisant des conditions de comparaison avec les labels du pic. La force de cette technique est sa complétude, c-a-d que toute relation confluente peut-être équippée d'un système de labels (par des entiers) pour lequel tous ses pics possèdent des diagrammes décroissants. Ce résultat est basé sur un théorème assez ancien de Klop, qui définit pour les systèmes non-terminant, uneespèce de forme normale sous la forme d'une suite infinie de récritures élémentaires, appellée "dérivation cofinale".Dans une première partie, nous révisitons les résultats de van Oostrom, et en proposons une preuve différente dans le but de les généraliser au cas des calculs dits "modulo", c-a-d dans des quotients, qui mèlent des règles et deséquations. Cette généralisation inclue la complétude, en faisant intervenir une généralisation de lanotion de dérivation cofinale dans le cas des calculs cohérents au sens de Jouannaud et Kirchner.La second partie de la thèse applique le théorème de van Oostrom et sa généralisation à des système (concrets) de récriture de termes, ainsi qu'à plusieurs priblèmes ouverts du domaine. L'application récente à des problèmes d'ordre supérieur tirés de la théorie des types dépendants ne fait pas partie de la thèse.
Type de document :
Thèse
Computation and Language [cs.CL]. Université Paris-Saclay, 2016. English. 〈NNT : 2016SACLX044〉
Liste complète des métadonnées

https://pastel.archives-ouvertes.fr/tel-01515698
Contributeur : Abes Star <>
Soumis le : vendredi 28 avril 2017 - 04:52:40
Dernière modification le : jeudi 10 mai 2018 - 02:06:54
Document(s) archivé(s) le : samedi 29 juillet 2017 - 12:26:49

Fichier

54418_LIU_2016_archivage.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01515698, version 1

Citation

Jiaxiang Liu. Confluence properties of rewrite rules by decreasing diagrams. Computation and Language [cs.CL]. Université Paris-Saclay, 2016. English. 〈NNT : 2016SACLX044〉. 〈tel-01515698〉

Partager

Métriques

Consultations de la notice

116

Téléchargements de fichiers

62