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

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

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

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

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

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

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 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

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é.