Skip to Main content Skip to Navigation
Theses

Etude des propriétés des systèmes de réécriture conditionnelle : mise en oeuvre de deux algorithmes de test de confluence sur les termes clos

Résumé : Définir un type abstrait algébrique par des axiomes conditionnels offre davantage de souplesse et de simplicité que dans un cadre classique, sans précondition. Ceci nous a amené à étudier la théorie conditionnelle de termes dans le but d'obtenir une méthode de décision fondée sur la réécriture de termes. Cependant, cette étude dans le contexte conditionnel soulève des problèmes délicats, principalement liés à la difficulté de formaliser la sémantique sous-jacente à la théorie conditionnelle et de définir des modèles. L'objectif de cette thèse est d'étudier les propriétés des systèmes de réécriture conditionnelle. Notre contribution centrale est la mise en œuvre de deux tests de confluence sur les termes clos. Le premier test est établi pour des systèmes de réécriture hiérarchiques, systèmes construits par strates successives, la précondition d'une règle utilisant exclusivement des opérateurs appartenant aux strates inférieures. Le second test de confluence est établi pour des systèmes décroissants, dont les règles sont définies avec un principe de récurrence structurelle sur leurs composantes. Ces deux classes de systèmes ont été définies et utilisées dans des travaux ultérieurs par divers auteurs pour éviter d'engendrer des dérivations infinies de réécriture. L'originalité du travail est l'utilisation d'un principe de raisonnement par cas, et la possibilité de réécrire une équation conditionnelle aussi bien dans sa partie conséquence que dans sa précondition. Ce processus de simplification s'est révélé souple et puissant et permet de traiter un certain nombre d'applications. Nous abordons également dans notre étude un aspect inhérent à la théorie conditionnelle : le comportement d'une spécification conditionnelle par rapport aux booléens. Ce comportement est fidèle dès lors que les propriétés de consistance et de complétude par rapport à la sorte booléenne sont garanties, assurant de façon intuitive qu'il n'y a ni ajout de booléens, ni confusion entre les deux constantes de vérité true et false. La propriété de complétude d'une spécification conditionnelle est également abordée. Cette propriété étant indécidable même dans la théorie classique, sans préconditions, nous proposons un algorithme fondé sur le raisonnement par cas pour tester si une spécification conditionnelle est complète par rapport à l'ensemble de ses constructeurs. Cet algorithme combine une analyse structurelle par le calcul d'un ensemble de motifs et une analyse par cas par le biais d'un ensemble de conditions utilisées dans la réécriture. Cette condition suffisante de test permet d'appréhender une sous-classe relativement étendue de définitions conditionnelles
Document type :
Theses
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01751005
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 1:01:26 PM
Last modification on : Tuesday, January 29, 2019 - 1:21:55 AM

File

INPL_T_1990_BOUSDIRA_W.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01751005, version 1

Collections

Citation

Wadoud Bousdira. Etude des propriétés des systèmes de réécriture conditionnelle : mise en oeuvre de deux algorithmes de test de confluence sur les termes clos. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 1990. Français. ⟨NNT : 1990INPL080N⟩. ⟨tel-01751005⟩

Share

Metrics

Record views

58

Files downloads

21