## [Système de Réécriture de Termes](/fr/node/60825) Définition Un système formel composé d'un ensemble de règles de réécriture dirigées employées pour transformer des termes en d'autres termes par des remplacements dirigés par motifs et substitutions. ## Principe Principe Les règles de la forme l -> r s'appliquent aux occurrences d'instances de l dans un terme plus grand via le matching et la substitution ; l'application répétée produit des séquences de réduction dont les propriétés (terminaison, confluence) déterminent l'existence et l'unicité des formes normales. ## Démonstration Démonstration Avec les règles { f(a) -> b, f(x) -> g(x) } et le terme f(f(a)), on applique d'abord f(a) -> b sur l'occurrence interne pour obtenir f(b), puis éventuellement f(x) -> g(x) pour obtenir g(b) ; des ordres d'application différents peuvent conduire à des issues différentes si le système n'est pas confluent. ## Mauvaise application Mauvaise application S'attendre à des formes normales uniques ou à la terminaison d'un TRS sans vérifier la confluence ou la terminaison ; appliquer des règles en ignorant la capture de variables ou des conditions contextuelles nécessaires au format de la règle. ## Conséquence Conséquence Conçu avec les propriétés voulues, un TRS fournit une normalisation algorithmique, des procédures de décision pour des théories équationnelles et une sémantique opérationnelle pour langages et démonstrateurs. ## Inversion Inversion Inverser la direction en traitant les règles comme des équations bidirectionnelles (l ↔ r) pour former une théorie équationnelle ; on perd la direction computationnelle et l'attention passe du calcul à la raison sur l'égalité. ## Limite Limite S'applique à des termes du premier ordre pour une signature et un ensemble de règles donnés ; les TRS standards excluent les constructions du lambda-calcul, les opérations à effets de bord ou les contraintes contextuelles sauf extension explicite. ## Tension sémantique Tension sémantique Tension entre la lecture des règles comme pas computationnels déterministes (réécriture) et comme égalités logiques (équations) où la direction et la stratégie deviennent secondaires ; les deux vues influencent les critères de correction. ## Synthèse Synthèse Un Système de Réécriture de Termes est un moteur syntaxique composé de règles de remplacement dirigées qui, par matching et substitution, réalisent des transformations de termes ; son utilité repose sur des propriétés méta comme terminaison et confluence qui contrôlent déterminisme et décidabilité.