Unification

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Unification (homonymie).

En informatique et en logique, un problème d'unification est un système d'équations qui portent sur des termes.

Quelques exemples[modifier | modifier le code]

Le problème d'unification

f(x,y) = f(a,g(x))

a une solution

x = a, y = g(a)

car substituer le terme a à la variable x et le terme g(a) à la variable y, dans les deux termes f(x,y) et f(a,g(x)) donne le même terme f(a,g(a)). Le problème d'unification

f(a,x) = f(a,g(y))

a une infinité de solutions

x = g(f(a,a)), y = f(a,a)
x = g(f(a,w)), y = f(a,w)
x = g(z), y = z
etc.

En revanche, le problème d'unification

f(x,y) = h(a,x)

n'a pas de solution et le problème d'unification

x = g(x)

non plus.

Le problème d'unification

x + 3 = 2 + 3

(c'est-à-dire +(x,3) = + (2,3)) a la solution x = 2, car substituer le terme 2 à la variable x dans les deux termes x + 3 et 2 + 3 donne le même terme 2 + 3. En revanche le problème d'unification

x + 3 = 5

n'a pas de solution, car en substituant un terme à la variable x, on ne peut pas rendre les deux termes x + 3 et 5 identiques. Cet objectif de rendre les deux termes absolument identiques est ce qui distingue les problèmes d'unification des équations algébriques habituelles.

Solution principale[modifier | modifier le code]

Une solution \sigma_2 d'un problème d'unification est dite plus générale qu'une solution \sigma_1, si \sigma_1 est obtenue en substituant des termes à des variables dans \sigma_2.

Par exemple, la solution

\sigma_2 = (x = g(f(a,w)), y = f(a,w))

du problème d'unification

f(a,x) = f(a,g(y))

est plus générale que la solution

\sigma_1 = (x = g(f(a,a)), y = f(a,a))

qui est obtenue en substituant le terme a à la variable w dans \sigma_2. De même, la solution

\sigma_3 = (x = g(z), y = z)

est plus générale que la solution \sigma_2, qui est obtenue en substituant le terme f(a,w) à la variable z dans la solution \sigma_3.

Une solution \sigma d'un problème d'unification est dite principale si elle est plus générale que toutes les solutions de ce problème, c'est-à-dire si toute solution est obtenue en substituant des termes à des variables dans \sigma.

Dans cet exemple, la solution \sigma_3 est une solution principale du problème

f(a,x) = f(a,g(y))

Le théorème de la solution principale exprime que si un problème d'unification a une solution, alors il a une solution principale.

Calcul d'une solution principale[modifier | modifier le code]

L'algorithme de Robinson permet de décider si un problème d'unification a des solutions ou non et, quand il en a, de calculer une solution principale.

On choisit une équation dans le système.

Si cette équation a la forme

f(t_1,\ldots,t_n) = f(u_1,\ldots,u_n)

on la remplace par les équations t_1 = u_1, ..., t_n = u_n et on résout le système obtenu.

Si cette équation a la forme

f(t_1,\ldots,t_n) = g(u_1,\ldots,u_m)

f et g sont des symboles différents, on échoue.

Si cette équation a la forme

x = x

on la supprime du système et on résout le système obtenu.

Si cette équation a la forme


x = t

ou


t = x

x apparaît dans t et est distinct de t, on échoue.

Si cette équation a la forme

x = t

ou

t = x

et que x n'apparaît pas dans t, on substitue le terme t à la variable x dans le reste du système, on résout le système obtenu, ce qui donne une solution \sigma et on retourne la solution \sigma, x = \sigma t.

Filtrage[modifier | modifier le code]

Un problème de filtrage est un problème d'unification dans lequel, dans chaque équation, les variables n'apparaissent que dans le terme de gauche. Par exemple, le problème

f(a,x) = f(a,g(b))

est un problème de filtrage, car le terme f(a,g(b)) ne contient pas de variables.

Dans le cas du filtrage, l'algorithme de Robinson se simplifie.

On choisit une équation dans le système.

Si cette équation a la forme

f(t_1,\ldots,t_n) = f(u_1,\ldots,u_n)

on la remplace par les équations t_1 = u_1, ..., t_n = u_n et on résout le système obtenu.

Si cette équation a la forme

f(t_1,\ldots,t_n) = g(u_1,\ldots,u_m)

f et g sont des symboles différents, on échoue.


Si cette équation a la forme

x = t

on substitue le terme t à la variable x dans le reste du système, on résout le système obtenu, ce qui donne une solution \sigma et on retourne la solution \sigma, x = t.

Histoire[modifier | modifier le code]

Le premier chercheur à évoquer un algorithme d'unification est Jacques Herbrand dans sa thèse, mais en fait l'unification a été redécouverte par John Alan Robinson dans le cadre de sa méthode de résolution en démonstration automatique. C'est lui qui lui donna son nom actuel. Une étape importante est ensuite la découverte d'algorithmes linéaires par Martelli et Montanari, Paterson et Wegman et Huet. Prolog a aussi beaucoup contribué à sa popularisation. Des algorithmes spécifiques pour les termes de certaines théories, appelés aussi unification équationnelle (en particulier associative et commutative par Stickel) ont été proposés (voir ci-dessus).

Utilisation de l'unification et du filtrage dans les langages de programmation[modifier | modifier le code]

L'unification est sans doute ce qui distingue le plus Prolog des autres langages de programmation.

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.

Exemples d'unification en prolog[modifier | modifier le code]

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

Unification équationnelle[modifier | modifier le code]

Unification et logique d'ordre supérieur[modifier | modifier le code]

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_1 et t_2 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_1 et t_2 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.


Sur les autres projets Wikimedia :