Unification (logique)

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 langage de programmation.

L'unification de deux termes et consiste à  trouver (quand il en existe) un troisième terme tel qu'on puisse passer de à  et à  en instanciant certaines variables. est alors appelé un unificateur de et . Intuitivement, l'unification est le fait d'attribuer une valeur à  certaines variables de et 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 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 re pré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ée 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 suite d'unifications ne joue (habituellement) aucun rà´le.

Unification et logique d'ordre supérieur

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 et 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 tel que tous les autres unificateurs de et soient dérivables par instantiation de variables de .

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.

Exemples d'unification en prolog

On supposera que toute 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 nombres 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(...)))). 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