Une application des variables vers des termes qui, appliquée à un terme ou une formule, remplace chaque variable de son domaine par le terme correspondant et s'étend homomorphiquement aux termes composés.

Principe

Une substitution sigma = { x1 -> t1, ..., xn -> tn } s'étend aux termes en remplaçant les variables et en appliquant sigma récursivement aux arguments de fonctions ; la composition et la restriction obéissent à des lois algébriques et interagissent avec la liaison de variables et la capture.

Démonstration

Avec sigma = { x -> f(a), y -> b }, appliquer sigma au terme g(x,y,z) donne g(f(a), b, z). En unification, on cherche une substitution rendant deux termes identiques, par exemple unifier f(x,a) et f(b,y) donne { x->b, y->a }.

Mauvaise application

Appliquer une substitution en présence d'assembleurs (par ex. abstractions lambda) sans renommer les variables liées conduit à la capture de variables ; supposer que la composition des substitutions est commutative ou que les substitutions sont inversibles sans vérification est également faux.

Conséquence

Les substitutions concrétisent des termes schématiques en termes concrets, permettent l'unification et le matching, pilotent l'application des règles en réécriture et sont fondamentales pour les étapes d'inférence en logique et en raisonnement automatique.

Inversion

Considérer l'anti-substitution ou l'abstraction de motif qui extrait une substitution faisant apparaître un terme concret à partir d'un motif ; l'anti-substitution est souvent partielle ou non unique, inverser une substitution est plus délicat que l'application directe.

Limite

Définie pour les variables libres des termes et formules du premier ordre ; la sémantique de la substitution doit être adaptée ou restreinte en présence de liants, de variables d'ordre supérieur ou de méta-variables, et il faut veiller à éviter la capture.

Tension sémantique

Tension entre la substitution syntaxique (remplacement textuel dans les termes) et l'affectation sémantique (application des variables à des valeurs dans un modèle) : la substitution syntaxique modifie la structure du terme tandis que l'affectation sémantique concerne valuation et vérité.

Synthèse

Une substitution est une application algébrique des variables vers des termes, étendue homomorphiquement aux expressions composées ; c'est le mécanisme qui instancie les variables, fonde l'unification et la réécriture, et nécessite des précautions anti-capture en présence de liants.