## [Unification](/fr/node/59919) Définition Le processus consistant à trouver des substitutions pour les variables qui rendent deux expressions syntaxiques (termes) identiques selon l'algèbre des termes d'une logique ; il produit une substitution associant variables à termes lorsqu'une solution existe. ## Principe Principe Résoudre un ensemble fini d'équations de termes en décomposant répétitivement les termes composés, en orientant les égalités impliquant des variables, en appliquant un test d'occurrence pour éviter les substitutions cycliques, et en calculant l'unificateur le plus général lorsque cela est possible. ## Démonstration Démonstration Unifier f(x, a) et f(b, y) donne la substitution {x ↦ b, y ↦ a}. En résolution du premier ordre, l'unification sert à rendre les littéraux syntaxiquement identiques avant d'appliquer la règle de résolution. ## Mauvaise application Mauvaise application Omettre la vérification d'occurrence et accepter des substitutions telles que x ↦ f(x) conduit à des termes cycliques ou mal fondés ; ou supposer que l'unification produit toujours une substitution unique alors que, dans des cadres théoriques ou d'ordre supérieur, il peut y avoir plusieurs unificateurs non comparables ou aucun. ## Conséquence Conséquence Appliquée correctement, l'unification fournit les substitutions nécessaires pour la démonstration automatique, la programmation logique et l'inférence de types ; l'unificateur le plus général conserve la généralité maximale, facilitant la réutilisation et la composition des preuves ou des programmes. ## Inversion Inversion La notion inverse est l'anti-unification (généralisation), qui trouve la généralisation la moins générale de deux termes plutôt qu'une substitution les rendant égaux ; conceptuellement, l'inversion passe de la résolution d'équations à la recherche d'une structure commune. ## Limite Limite L'unification standard (du premier ordre) suppose une algèbre syntaxique des termes sans théories intégrées ; elle exclut l'unification équationnelle ou modulo théorie (par exemple modulo associativité ou commutativité) et l'unification d'ordre supérieur sauf indication contraire, chacune nécessitant des algorithmes et ayant des propriétés de décidabilité différentes. ## Tension sémantique Tension sémantique Il existe une tension entre l'unification et le patronnage (pattern matching) : le patronnage fixe un côté comme motif à instancier, produisant des substitutions unidirectionnelles spécialisées, tandis que l'unification est symétrique et peut renvoyer des substitutions plus générales ; autre tension entre unification syntactique et unification équationnelle (sensible à la théorie). ## Synthèse Synthèse L'unification est un solveur algorithmique pour des équations syntaxiques de termes : en décomposant les structures, en imposant des contraintes d'occurrence et en calculant des unificateurs les plus généraux, elle fournit les substitutions qui permettent l'instanciation de variables dans l'inférence, la programmation et la vérification de types.