Preuves de terminaison des systèmes de réecriture : un outil fondé sur les interprétations polynomiales / Ahlem Ben Cherifa ; Sous la direction de Pierre Lescanne

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Réécriture, Systèmes de (informatique)

Polynômes

Lescanne, Pierre (1947-....) (Directeur de thèse / thesis advisor)

Université Henri Poincaré Nancy 1. Faculté des sciences et techniques (Autre partenaire associé à la thèse / thesis associated third party)

Université de Nancy I (1970-2012) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : L'objectif de cette thèse est une étude de la terminaison des systèmes de réécriture de termes en utilisant des interprétations polynomiales. Nous caractérisons aussi les interprétations polynomiales des opérateurs associatifs cumutatifs (ou AC), fournissant ainsi un nouvel ordre, utilisant le même processus que celui adopté pour la terminaison de la réécriture standard. De plus nous avons veillé à utiliser le principe de la terminaison associative-commutative, pour l'étendre à d'autres catégories de réécriture équationnelle. Enfin nous étendons notre approche aux produits cartésiens sur les polynômes, permettant ainsi l'utilisation de plus d'une interprétation pour un symbole de fonction donné. Nous utilisons alors, pour la preuve de la terminaison, les interprétations polynomiales classiques ou les interprétations polynomiales associatives-commutatives et un ordre lexicographique. Un autre problème a été abordé dans sa généralité au cours de ce travail: il s'agit de la détermination des bonnes interprétations polynomiales. En nous fondant sur notre expérience, nous avons pu fournir à l'utilisateur quelques bonnes suggestions afin de l'aider dans le choix de ses interprétations.