Le processus algorithmique consistant à trouver une substitution (application de variables à termes) qui rend deux expressions symboliques identiques au sens de l'égalité syntaxique (ou modulo une théorie) ; central en raisonnement automatique, inférence de types et programmation logique.

Principe

Rechercher un unificateur le plus général (mgu) qui résout les équations d'appariement entre sous-termes correspondants sans introduire d'instanciations inutiles ; la vérification d'occurrence (occur‑check) évite les substitutions cycliques, et les variantes incluent l'unification syntaxique du premier ordre, l'E‑unification (modulo théories équationnelles) et l'unification d'ordre supérieur avec des profils de décidabilité et de complexité très différents.

Démonstration

Exemple du premier ordre : unifier f(x,a) et f(b,y) — le mgu est {x↦b, y↦a}. Exemple d'occur‑check : unifier x et f(x) échoue car toute solution serait cyclique (en unification du premier ordre l'occur‑check rejette cela). Exemple d'ordre supérieur : l'unification dans le λ-calcul est indécidable en général et nécessite des algorithmes différents (p. ex. procédures semi‑décidables de Huet) ou des restrictions pour obtenir la décidabilité.

Mauvaise application

Omettre l'occur‑check dans des implémentations produit des substitutions non valides qui permettent des termes infinis et des réponses erronées. Appliquer des algorithmes d'unification du premier ordre à des problèmes impliquant opérateurs associatifs/commutatifs ou des liaisons d'ordre supérieur sans utiliser la machinerie E‑unification ou d'ordre supérieur appropriée conduit à une unification incorrecte ou incomplète.

Conséquence

L'unification fournit les substitutions nécessaires à la résolution en démonstration du premier ordre, à l'inférence de types dans les langages de programmation et à l'appariement dans les systèmes de réécriture ; lorsque des mgu existent ils permettent des solutions générales et réutilisables, tandis que l'intractabilité ou l'indécidabilité dans des cadres plus expressifs contraint le raisonnement automatique et impose heuristiques ou fragments restreints.

Inversion

Le matching (unification unilatérale) restreint les variables à une seule expression et est computationnellement plus simple ; l'anti‑unification (généralisation) calcule des généralisateurs les moins généraux plutôt que des unificateurs les plus généraux. Inverser l'unification déplace conceptuellement de la résolution d'équations vers la recherche d'abstractions schématiques.

Limite

L'unification syntaxique du premier ordre est décidable et possède des unificateurs les plus généraux lorsqu'elle est solvable ; l'unification modulo théories (AC, associatif‑commutatif, etc.) ou l'unification d'ordre supérieur peut être indécidable ou de complexité beaucoup plus élevée. Les propriétés exactes dépendent de la logique et de la théorie considérées.

Tension sémantique

Tension entre l'unification syntaxique (structure pure des termes) et l'unification sémantique (modulo théories) affecte à la fois la complétude et les performances ; des compromis apparaissent entre un raisonnement équationnel plus riche et la tractabilité algorithmique.

Synthèse

L'unification est le processus de calcul des substitutions qui rendent des termes égaux selon une notion d'égalité choisie ; opération centrale en déduction automatique et en systèmes de types, elle met en balance la recherche de solutions générales et réutilisables avec les limites imposées par l'occurence, les théories équationnelles et les caractéristiques d'ordre supérieur, qui modifient la décidabilité et la complexité.