Execution models for Constraint Programming: kernel language design through semantics equivalence.

Résumé : La programmation logique et la programmation par contraintes sont deux paradigmes de programmation déclaratifs qui reposent sur l'identification entre programmes et théories logiques d'une part, et entre programmation et modélisation d'autre part. Les modèles d'exécution résultent de l'interprétation opérationnelle de la prouvabilité logique en programmation logique, et de la propagation des contraintes en programmation par contraintes. Cependant, le contrôle de l'exécution est crucial pour rendre ces paradigmes utilisables en pratique et des traits extra-logiques sont ajoutés à cette fin dans ces systèmes de programmations, avec les slogans classiques « programmation logique = théorie logique + contrôle » et « programmation par contraintes = modèle de contraintes + recherche ». Cette thèse explore des modèles d’exécution au sein desquels le contrôle et la recherche peuvent être remontés selon le contexte dans la logique ou dans le modèle de contraintes, tout en préservant la sémantique. Les trois parties de cette thèse correspondent aux trois équivalences sémantiques démontrées : la première entre deux langages logiques en chaînage avant avec choix commis, la seconde entre programmes logiques avec contraintes et modèles de contraintes, la troisième entre les sémantiques des gardes dans un cadre angélique. Chacune de ces équivalences est constructive au sens qu’il existe un codage permettant la compilation depuis l’un des paradigmes dans l’autre. Premièrement, nous montrons que des transformations simples de programmes existent dans les deux sens entre les langages Constraint Handling Rules (CHR) et Linear Logic Concurrent Constraint (LLCC), les rendant sémantiquement équivalents bien que syntaxiquement différents, ce qui ferme la question de l'implémentation d'une sémantique de choix commis pour LLCC, en utilisant CHR comme langage noyau. Deuxièmement, nous montrons qu'une large variété de procédures de recherche peut être internalisée dans le modèle de contraintes avec une stratégie d'énumération fixe. La transformation de procédures de recherche en problèmes de satisfaction de contraintes présente plusieurs avantages : (1) cela rend les stratégies de recherche déclaratives et modélisables au même titre que les problèmes de satisfaction de contraintes ; (2) cela rend possible l'expression de stratégies de recherche dans les langages de modélisation existants, sans recourir à des extensions ; (3) cela ouvre la voie à des algorithmes de propagation de contraintes pour les contraintes de recherche et à l'implémentation de nouvelles procédures de recherche basées sur la propagation de contraintes. Ceci est illustré par la conception du langage de modélisation ClpZinc, avec une interprétation angélique des clauses de Horn qui permet la compilation vers un noyau de contraintes basé sur la réification. Pour finir, en programmation concurrente avec contraintes, la sémantique par choix commis crée une hiérarchie de sémantiques non équivalentes axée sur la puissance d'expression des mécanismes de synchronisation. Nous montrons que la hiérarchie des gardes s'effondre avec la sémantique angélique, permettant au plus primitif des mécanismes de synchronisation de coder tous les autres. La principale conséquence de cet effondrement est l'identification d'un langage noyau, avec un mécanisme de synchronisation primitif et un système de contraintes élémentaires qui sont suffisants pour reconstruire les autres formes de synchronisation et les autres systèmes de contraintes comme modules, au sens de l'ingénierie logicielle.
Mots-clés : pas de mots-clés
Type de document :
Thèse
Programming Languages [cs.PL]. Paris Diderot, 2015. English
Liste complète des métadonnées

Littérature citée [76 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01251695
Contributeur : Sylvain Soliman <>
Soumis le : mercredi 6 janvier 2016 - 15:51:31
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : jeudi 7 avril 2016 - 16:05:36

Fichier

Identifiants

  • HAL Id : tel-01251695, version 1

Collections

Citation

Thierry Martinez. Execution models for Constraint Programming: kernel language design through semantics equivalence. . Programming Languages [cs.PL]. Paris Diderot, 2015. English. 〈tel-01251695〉

Partager

Métriques

Consultations de la notice

185

Téléchargements de fichiers

163