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 - Université de Lorraine Access content directly
Theses Year : 1990

Study of conditional term rewriting system properties. Making use of two algorithms for testing confluence on ground terms

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

Wadoud Bousdira
  • Function : Author
  • PersonId : 763067
  • IdRef : 084091533

Abstract

Not available
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
Fichier principal
Vignette du fichier
INPL_T_1990_BOUSDIRA_W.pdf (26.19 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

tel-01751005 , version 1 (29-03-2018)

Identifiers

  • HAL Id : tel-01751005 , version 1

Cite

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. Informatique [cs]. Institut National Polytechnique de Lorraine, 1990. Français. ⟨NNT : 1990INPL080N⟩. ⟨tel-01751005⟩
92 View
17 Download

Share

Gmail Facebook X LinkedIn More