Unification

Le concept d'unification est une notion centrale de la logique des prédicats ainsi que d'autres systèmes de logique et est sans doute ce qui distingue le plus Prolog des autres langages de programmation.

L'unification de deux termes t₁ et t₂ consiste à trouver (quand il en existe) un troisième terme t tel qu'on puisse passer de t à t₁ et à t₂ en instanciant certaines variables. t est alors appelé un unificateur de t₁ et t₂. Intuitivement, l'unification est le fait d'attribuer une valeur à certaines variables de t₁ et t₂ et peut être regardé comme un genre d'assignation qui ne pourrait s'effectuer qu'une seule fois. Lorsqu'on résout une équation algébrique, une inconnue peut avoir une, plusieurs ou aucune solutions, mais sa valeur ne change pas durant les opérations; c'est pareil pour l'unification. En fait on peut voir la résolution d'une équation comme un cas particulier d'unification.

En prolog, cette opération est dénotée par symbole « = ». Les règles de l'unification sont les suivantes:

1. une variable X non-instanciée (c'est-à-dire ne possédant pas encore de valeur) peut être unifiée avec une autre variable (instanciée ou pas); les deux variables deviennent alors simplement des synonymes l'une de l'autre et représenteront dorénavant la même chose ;
2. une variable X non-instanciée peut être unifiée avec un terme ou un atome et représentera dorénavant ce terme ou atome ;
3. un atome peut être unifié seulement avec le même atome ;
4. un terme peut être unifié avec un autre terme : si leurs noms sont identiques, si leur nombres d'arguments sont identiques et si chacun des arguments du premier terme est (récursivement) unifiable avec l'argument correspondant du second terme.

En raison de sa nature déclarative, l'ordre dans une suite d'unifications ne joue (habituellement) aucun rôle.

Lorsqu'on raisonne en logique du premier ordre, où les variables ne peuvent être unifiées qu'à des constantes, les choses se passent bien: savoir si deux termes t₁ et t₂ sont unifiables est décidable (grâce par exemple à l'algorithme ci-dessus). De plus, s'ils le sont, il existe un unificateur le plus général (most general unifier ou mgu en anglais), c'est-à-dire un terme t tel que tous les autres unificateurs de t₁ et t₂ soient dérivables par instantiation de variables de t.

Cette situation idéale ne se retrouve hélas pas dans tous les systèmes logiques. En particulier, si on se place en logique d'ordre supérieur, c'est-à-dire qu'on s'autorise à utiliser des variables comme symboles de fonction ou comme prédicats, on perd la décidabilité et l'unicité de l'unificateur quand il existe. Au pire, deux termes peuvent même avoir une infinité d'unificateurs tous différents.

On supposera que toutes les variables (en majuscules) sont non-instanciées.

A = A

réussit (tautologie)

A = B, B = abc

A et B sont unifiés avec l'atome 'abc'

xyz = C, C = D

réussit: l'unification est symétrique

abc = abc

réussit: les atomes sont identiques

abc = xyz

échoue: des atomes distincts ne s'unifient pas

f(A) = f(B)

réussit: A est unifié avec B

f(A) = g(B)

échoue: les termes ont des noms différents

f(A) = f(B, C)

échoue: les termes ont un nombre d'arguments différents

f(g(A)) = f(B)

réussit: B est unifié au terme g(A)

f(g(A), A) = f(B, xyz)

réussit: B est unifié au terme g(xyz) et A est unifié à l'atome 'xyz'

A = f(A)

l'unification est infinie: A est unifié au terme f(f(f(f(f(...)))). Suivant le système logique que l'on souhaite on peut considérer que l'unification échoue ou réussit; la plupart de ces systèmes considèrent que l'unification échoue.

A = abc, xyz = X, A = X

échoue: car abc=xyz échoue