Abstract FR:

La réécriture est, à plusieurs titres (programmation fonctionnelle, logico-fonctionnelle équationnelle), un paradigme de la programmation. Notre approche se situe en amont de la programmation et à pour but de contribuer à une meilleure connaissance des arbres et de la réécriture dans les arbres. Nous utilisons, en particulier, la théorie des automates d'arbres. Les résultats principaux de notre travail sont les suivants : 1) nous étudions les problèmes de décidabilité sur les systèmes de réécriture et les forêts reconnaissables. En particulier, nous étudions la propriété (P) : pour toute forêt reconnaissable, l'ensemble des formes normales des termes de F pour S est reconnaissable. Nous prouvons l'indécidabilité de cette propriété. Nous prouvons l'indécidabilité du fragment existentiel de théorie dans l'algèbre des termes clos quotientée par la relation de congruence définie par un ensemble d'équations E, lorsqu'il existe un système de réécriture S convergent, adéquat pour E et satisfaisant (P). Nous présentons un algorithme de décision pour une sous classe de formules linéaires d'une telle théorie ; 2) nous montrons que le problème d'accessibilité est décidable pour les systèmes de réécriture clos modulo la commutativité (complexité polynomiale), est indécidable modulo l'associativité et décidable (résultat partiel) dans le cas associatif et commutatif (équivalent au problème d'accessibilité pour les vecteurs addition systèmes) ; 3) nous introduisons une notion qui permet d'éclairer et de généraliser les études antérieures sur les liens entre systèmes de réécriture et automates à piles.