Structures et modèles de calculs de réécriture

• Main Author: Faure, Germain
• Language: FRE
• Published: Université Henri Poincaré - Nancy I 2007
• Subjects: [INFO:INFO_SE] Computer Science/Software Engineering; Filtrage; lambda-calcul; calculs de réécriture; calculs de motifs; filtrage d'ordre supérieur; super-développements; calculs explicites; confluence; sémantique catégorique; lambda-calcul parallèle; modèles syntaxiques
• Online Access: http://tel.archives-ouvertes.fr/tel-00164576; http://tel.archives-ouvertes.fr/docs/00/16/45/76/PDF/manuscript.pdf

Le calcul de réécriture ou rho-calcul est une généralisation du lambda-calcul avec filtrage et agrégation de termes. L'abstraction sur les variables est étendue à une abstraction sur les motifs et le filtrage correspondant peut être effectué modulo une théorie <br />équationnelle a priori arbitraire. L'agrégation est utilisée pour collecter les différents résultats possibles.<br />Dans cette thèse, nous étudions différentes combinaisons des ingrédients fondamentaux du rho-calcul: le filtrage, l'agrégation et les mécanismes d'ordre supérieur.<br />Nous étudions le filtrage d'ordre supérieur dans le lambda-calcul pur modulo une restriction de la beta-conversion appelée super-développements. Cette nouvelle approche est suffisamment expressive pour traiter les problèmes de filtrage du second-ordre et ceux avec des motifs d'ordre supérieur à la Miller.<br />Nous examinons ensuite les modèles catégoriques du<br />lambda-calcul parallèle qui peut être vu comme un enrichissement du lambda-calcul avec l'agrégation de termes. Nous montrons que ceci est une étape significative vers la sémantique dénotationnelle du calcul de réécriture.<br />Nous proposons également une étude et une comparaison des calculs avec motifs éventuellement dynamiques, c'est-à-dire qui peuvent être instanciés et réduits. Nous montrons que cette étude, et plus particulièrement la preuve de confluence, est suffisamment générale pour<br />s'appliquer à l'ensemble des calculs connus. Nous étudions ensuite l'implémentation de tels calculs en proposant un calcul de réécriture avec filtrage et substitutions explicites.