Transformations de programmes logiques avec contraintes.

BENSAOU Nacera

IBP-Litp 1996/Th/05: THÈSE de DOCTORAT de l'UNIVERSITÉ PARIS 6 Litp / Litp research reports
140 pages - Octobre/October 1996 - French document.

PostScript : Ko /Kb

Titre / Title: Transformations de programmes logiques avec contraintes.

Résumé : Nous étudions les transformations par dépliage/pliage des programmes CLP. Notre contribution dans ce domaine est l'extension des résultats de correction des programmes obtenus dans le cadre de la programmation logique au cadre de la programmation CLP.
Nous définissons pour nos programmes, une sémantique opérationnelle et une sémantique de point fixe basées sur la notion de C-modèles à laquelle nous ajoutons la notion explicite d'implication entre contraintes. Nous étendons le système de transformation de Tamaki-Sato aux programmes CLP. Les transformations que nous définissons sont : la règle de définition, le dépliage, le pliage, la règle de remplacement et des règles de simplification de clauses et de contraintes. Nous en donnons ensuite des preuves de correction totale basées sur l'opérateur TP. La première forme et la deuxième forme du pliage sont respectivement les extensions des pliages de Tamaki-Sato et de celui de Gardner-Shepherdson aux programmes CLP. Nous introduisons trois règles de remplacement d'une conjonction d'atomes contraints par une autre : la règle de substitition nécessite l'équivalence des deux conjonctions dans toute interprétation et pour toute substitution. Pour les deux autre formes, il suffit de valider cette équivalence seulement une fois, si les programmes ne sont soumis qu'à des transformations totalement correctes. La première forme étend la règle de remplacement de Gardner-Shepherdson aux programmmes CLP. La seconde forme, plus générale, est paramétrée par la sémantique. Enfin, nous appliquons à des programmes CLP linéaires récursifs la stratégie de fusion de boucles, proposée par Debray pour les programmes logiques.

Abstract : Nous étudions les transformations par dépliage/pliage des programmes CLP. Notre contribution dans ce domaine est l'extension des résultats de correction des programmes obtenus dans le cadre de la programmation logique au cadre de la programmation CLP.
Nous définissons pour nos programmes, une sémantique opérationnelle et une sémantique de point fixe basées sur la notion de C-modèles à laquelle nous ajoutons la notion explicite d'implication entre contraintes. Nous étendons le système de transformation de Tamaki-Sato aux programmes CLP. Les transformations que nous définissons sont : la règle de définition, le dépliage, le pliage, la règle de remplacement et des règles de simplification de clauses et de contraintes. Nous en donnons ensuite des preuves de correction totale basées sur l'opérateur TP. La première forme et la deuxième forme du pliage sont respectivement les extensions des pliages de Tamaki-Sato et de celui de Gardner-Shepherdson aux programmes CLP. Nous introduisons trois règles de remplacement d'une conjonction d'atomes contraints par une autre : la règle de substitition nécessite l'équivalence des deux conjonctions dans toute interprétation et pour toute substitution. Pour les deux autre formes, il suffit de valider cette équivalence seulement une fois, si les programmes ne sont soumis qu'à des transformations totalement correctes. La première forme étend la règle de remplacement de Gardner-Shepherdson aux programmmes CLP. La seconde forme, plus générale, est paramétrée par la sémantique. Enfin, nous appliquons à des programmes CLP linéaires récursifs la stratégie de fusion de boucles, proposée par Debray pour les programmes logiques.

Publications internes Litp 1996 / Litp research reports 1996