Unification

vignette|Unifier deux termes, c'est les rendre identiques en remplaçant les variables. En informatique et en logique, l'unification est un processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques. Par exemple, et peuvent être rendus identiques par la substitution et , qui donne quand on l'applique à chacun de ces termes le terme . Dit autrement, l'unification est la résolution d'une équation dans l'algèbre des termes (unification syntaxique) ou dans une algèbre quotient par un ensemble d'identités (unification modulo une théorie) ; la solution de l'équation est la substitution qui rend les deux termes identiques et que l'on appelle l'unificateur. L'unification a des applications en inférence de types, programmation logique, en démonstration automatique de théorèmes, en système de réécriture, en traitement du langage naturel.

Souvent, on s'intéresse à l'unification syntaxique où il faut que les termes obtenus par application de l'unificateur soient syntaxiquement égaux, comme dans l'exemple ci-dessus. Par exemple, le problème d'unification syntaxique ayant pour données et n'a pas de solutionAttention, n'est pas une solution car les termes et sont syntaxiquement différents.. Le filtrage par motif (ou pattern matching) est une restriction de l'unification où l'unificateur n'est appliquée qu'à un seul des deux termes. Par exemple, et sont rendus égaux par la substitution .

La fin de l'article présente aussi l'unification modulo une théorie, qui est le cas où on dispose de connaissances supplémentaires sur les fonctions (par exemple, est commutatif).

Histoire vignette|Jacques Herbrand en 1931, considéré comme le précurseur de l'unification vignette|John Alan Robinson, considéré comme le fondateur de l'unification.

Invention de la notion d'unification Le premier chercheur à évoquer un algorithme d'unification est Jacques Herbrand dans sa thèse en 1930. Il s'agit d'un algorithme non-déterministe pour unifier deux termes. Herbrand était intéressé par la résolution d'équations. En 1960, Prawitz et Voghera ont généralisé le calcul propositionnel à des formules du premier ordre non instanciées, ou tout au moins en les instanciant a minima. L'unification a ensuite été redécouverte en 1963, mais l'article qui la décrit est publié seulement en 1965, par John Alan RobinsonJohn Alan Robinson: Logic and Logic Programming. Commun. ACM 35(3): 40-65 (1992) dans le cadre de sa méthode de résolution en démonstration automatique. Selon Baader et Snyder, c'est Knuth et BendixDonald Knuth, All Questions Answered, 318. NOTICES OF THE AMS. VOLUME 49, NUMBER 3, en 1970, qui ont introduit le concept de "substitution la plus générale" dans leur travail sur la confluence locale d'un système de réécriture. Un an avant la publication de l'article de Robinson, soit en 1964, Guard a indépendamment étudié le problème d'unification sous le nom de matching.

Course vers l'efficacité L'algorithme originel de Robinson est inefficace car il s'exécute en temps exponentiel et demande une quantité de mémoire exponentielle. Robinson écrit alors une note en 1971 où il exhibe une représentation des termes plus concise. L'algorithme utilise alors un espace mémoire polynomial. Boyer et Moore donnent aussi un algorithme qui utilise un espace mémoire polynomial en temps exponentiel dans le pire cas. Venturini-Zilli introduit un système de marquage pour que l'algorithme de Robinson s'exécute en temps quadratique, dans le pire cas, en la taille des termes. Huet travaille sur l'unification d'ordre supérieur et améliore le temps d'exécution de l'algorithme syntaxique du premier ordre : son algorithme est quasi linéaire. D'autres chercheurs ont exhibé des algorithmes quasi linéaires.

Une étape importante est ensuite la découverte d'algorithmes linéaires en 1976 par Martelli et Montanari, Paterson et Wegman et Huet. Comme les articles de Paterson et Wegman sont courts, Dennis de Champeaux a réexpliqué l'idée de l'algorithme en 1986.

En 1982, Martelli et Montanari présentent un algorithme presque-linéaire mais plus efficace en pratique.

En 1984, Dwork et al. démontrent que l'unification est P-complet, ce qui signifie qu'a priori l'unification est difficile à paralléliser. Par opposition, le problème de filtrage par motif (pattern matching) est dans NC, c'est-à-dire facile à paralléliser.

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).

Description

Problèmes d'unification

Un problème d'unification peut être présenté comme la donnée de deux termes, ou alors comme une équation, ou alors comme un ensemble de termes à unifier, ou alors comme un ensemble de couples de termes, ou alors comme un ensemble d'équations. Le problème d'unification a une solution car substituer (i.e. remplacer) le terme à la variable et le terme à la variable , dans les deux termes et donne le même terme . En revanche, le problème d'unification n'a pas de solution et le problème d'unification non plus.

Solution principale

Un problème d'unification peut avoir une infinité de solutions. Par exemple, a une infinité de solutions : , , , etc. De toutes ces solutions, on exhibe des solutions dites principales car elles permettent de construire toutes les autres solutions : c'est le concept de solution principale, ou unificateur le plus général (most general unifier, mgu).

Tout d'abord, une solution d'un problème d'unification est dite plus générale qu'une solution , si est obtenue en substituant des termes à des variables dans . Par exemple, si on considère le problème d'unification , alors la solution est plus générale que la solution qui est obtenue en substituant le terme à la variable dans . De même, la solution est plus générale que la solution , qui est obtenue en substituant le terme à la variable dans la solution .

Une solution 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 . Dans cet exemple, la solution est une solution principale du problème.

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. Un algorithme d'unification calcule une solution principale ou échoue si les termes ne sont pas unifiables.

Exemples La table suivante donne des exemples de problèmes d'unification. En plus, nous donnons aussi, dans la colonne de gauche, les exemples avec la syntaxe de Prolog : une variable commence par une majuscule, les constantes et symboles de fonction commencent par une minuscule. Pour les notations mathématiques, x,y,z sont des variables, , f,g sont des symboles de fonction et a,b sont des constantes. Notation Prolog Notation mathématiqueSolution (principale)Explication a = a { a = a }{}L'unification réussit car nous avons le même symbole de constante a de part et d'autre de l'égalité. a = b { a = b }échoueL'unification échoue. En effet, a et b sont des symboles de constantes différents Donc il est impossible de rendre les deux termes de part et d'autre de l'égalité syntaxiquement égaux. X = X { x = x }{}L'unification réussit car nous avons la même variable de part et d'autre de l'égalité. a = X { a = x }{ x ↦ a }La variable x est unifié avec la constante a. X = Y { x = y }{ x ↦ y }La variable x est unifié avec y. f(a,X) = f(a,b) { f(a,x) = f(a,b) }{ x ↦ b }Les symboles de fonction sont les mêmes. x est unifié avec la constante b f(a) = g(a) { f(a) = g(a) }échouef et g sont des symboles de fonction différents. On ne peut donc pas rendre les deux termes syntaxiquement égaux. f(X) = f(Y) { f(x) = f(y) }{ x ↦ y }x est unifié avec y f(X) = g(Y) { f(x) = g(y) }échouef et g sont des symboles de fonction différents f(X) = f(Y,Z) { f(x) = f(y,z) }échoueLe symbole de fonction f est d'arité 1 dans la partie gauche et d'arité 2 dans la partie droite. f(g(X)) = f(Y) { f(g(x)) = f(y) }{ y ↦ g(x) }y est unifié avec g(x) f(g(X),X) = f(Y,a) { f(g(x),x) = f(y,a) }{ x ↦ a, y ↦ g(a) }x est unifié avec la constante a, et y est unifié avec g(a) X = f(X) { x = f(x) }échoueéchoue car x apparaît dans f(x). Le test d'appartenance de x dans le terme droit f(x) s'appelle occur check. Il existe des implémentations de Prolog où il n'y a pas d'occur check. Pour ces dernières, on unifie x avec le terme infini x=f(f(f(f(...)))). X = Y, Y = a { x = y, y = a }{ x ↦ a, y ↦ a }x et y sont unifiés avec la constante a a = Y, X = Y { a = y, x = y }{ x ↦ a, y ↦ a }x et y sont unifiés avec la constante a X = a, b = X { x = a, b = x }échouea et b sont des symboles de constantes différents. x ne peut s'unifier avec les deux à la fois.

Applications Filtrage par motif dans les langages de programmation

Le filtrage par motif est la restriction de l'unification dans laquelle, dans chaque équation, les variables n'apparaissent que dans le terme de gauche. Par exemple, le problèmeest un problème de filtrage, car le terme ne contient pas de variables. Le filtrage est utilisé dans les langages fonctionnels comme Haskell, Caml, LISP.

Dans le cas du filtrage, l'algorithme de Martelli et Montanari se simplifie.

On choisit une équation dans le système.

Si cette équation a la forme

on la remplace par les équations , ..., et on résout le système obtenu.

Si cette équation a la forme

où et sont des symboles différents, on échoue.

Si cette équation a la forme

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

Programmation logique

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

En Prolog, l’unification est associée au symbole « = » et ses règles sont les suivantes : 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 le même objet (ou la même structure) ; 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 ; un atome peut être unifié seulement avec lui-même ; un terme peut être unifié avec un autre terme : si leur symbole sont identiques, si leurs nombres d'arguments sont identiques et si chacun des arguments du premier terme est unifiable avec l'argument correspondant du second terme.

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

Algorithmes Algorithme de Robinson L'algorithme de Robinson de 1965 a été reformulé, par Corbin et Bidoit en 1983 Jacques Corbin, Michel Bidoit: A Rehabilitation of Robinson's Unification Algorithm. IFIP Congress 1983: 909-914, puis amélioré par Ruzicka et Prívara en 1989Peter Ruzicka, Igor Prívara: An Almost Linear Robinson Unification Algorithm. Acta Inf. 27(1): 61-71 (1989),