Anti-unification

Modèle:Confusion En informatique théorique et en logique mathématique, lModèle:'anti-unification est la construction d'une généralisation commune à deux termes symboliques données. Comme son nom l’indique, c'est l'Modèle:Passage évasif de l'unification qui est le calcul de l'instance la plus générale des termes.

Des problèmes d'anti-unification se posent dans de nombreuses branches de l'intelligence artificielle : apprentissage machine, raisonnement analogique et basé sur des cas, modélisation cognitive, découverte de connaissances, etc. L'anti-unification est une technique souvent utilisée pour résoudre les problèmes de généralisation. Comme pour l’unification, on distingue plusieurs niveaux selon la nature des termes considérés du premier ordre ou d'ordre supérieur, termes nominaux, arbres, et autres.

Présentation

Un terme $t$ est une généralisation de deux termes $t_1$ et $t_2$ si $t_1=t{\eta }_1$ et $t_2=t{\eta }_2$, pour des substitutions ${\eta }_1$ et ${\eta }_2$. Une généralisation $t$ de $t_1$ et $t_2$ est minimale, ou la plus spécifique, si pour toute généralisation $t^{\prime }$ de $t_1$ et $t_2$, il existe une substitution $\xi$ telle qui $t=t^{\prime }\xi$. Le problème de l'anti-unification est le calcul de la généralisation minimale de deux termes donnés. Ce problème et Modèle:Passage évasif du problème d'unification, qui est le calcul de l'instance la plus générale de termes. En absence de variables représentant des fonctions dans les termes, le processus est une anti-unification du premier ordre, sinon est une anti-unification d'ordre supérieur.

Un algorithme d'anti-unification calcule, pour des termes données, un ensemble complet et minimal de généralisations, c'est-à-dire un ensemble couvrant toutes les généralisations et ne contenant aucun élément redondant. Selon le cadre, un ensemble de généralisation complet et minimal peut avoir un, plusieurs ou même un nombre infini d'éléments, ou peut ne pas exister du tout ; il ne peut pas être vide, puisqu'une généralisation triviale existe dans tous les cas. Pour l'anti-unification syntaxique du premier ordre, Gordon PlotkinModèle:, a donné un algorithme qui calcule un ensemble singleton qui est complet et minimal, la « plus petite généralisation ».

L'anti-unification est différente de la Modèle:Lien. Cette dernière consiste à résoudre des systèmes de « diséquations » (c'est-à-dire de la forme $e\ne e^{\prime }$), donc de trouver des valeurs des variables pour lesquelles toutes les dis-égalités données sont satisfaites.

Cadre

Termes

L'anti-unification se réalise dans une cadre logique où sont donnés :

• Un ensemble infini V de variables.
• Un ensemble T de termes contenant V. Pour l'anti-unification du premier ordre ou d'ordre supérieur, T est en général formé des termes du premier ordre (variables et symboles de fonction) et de termes du lambda-calcul respectivement.
• Une relation d'équivalence $\equiv$ sur $T$, indiquant quels termes sont considérés comme égaux. Pour l'unification d'ordre supérieur, on a $t\equiv u$ si $t$ et $u$ sont alpha equivalents. Pour le premier ordre, $\equiv$ représente une certaine connaissance sur les symboles de fonction ; si par exemple $\oplus$ est commutative, on a $t\equiv u$ si $u$ et $t$ sont les mêmes par échange d'arguments de $\oplus$ dans certaines ou toutes les occurrences. Si aucune information n'est disponible, l'équivalence se réduit à l'égalité.

Substitution

Une substitution est une application $\sigma :V\to T$ des variables dans des termes ; le résultat de l'application d'une substitution $\sigma$ à un terme $t$ est appelé une instance de $t$.

Par exemple, l'application de la substitution $\{x\mapsto h(a,y),z\mapsto b\}$ au terme $f(x,a,g(z),y)$ produit $f(h(a,y),a,g(b),y)$.

Généralisation et spécialisation

Si un terme $t$ a une instance qui est équivalente à un terme $u$, c'est-à-dire si $t\sigma \equiv u$ pour une substitution $\sigma$, alors $t$ est dit plus général que $u$, et $u$ est appelé plus particulier que $t$. Par exemple, $x\oplus a$ est plus général que $a\oplus b$ si $\oplus$ est commutative, puisque$(x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b$.

Si $\equiv$ est l'identité littérale (syntaxique) de termes, un terme peut être à la fois plus général et plus particulier qu'un autre seulement si les deux termes ne diffèrent que par les noms de leurs variables, et non par leur structure syntaxique ; ces termes sont appelés variantes, ou renommages l'un de l'autre. Par exemple, $f(x_1,a,g(z_1),y_1)$ est une variante de $f(x_2,a,g(z_2),y_2)$, puisque $f(x_1,a,g(z_1),y_1)\{x_1\mapsto x_2,y_1\mapsto y_2,z_1\mapsto z_2\}=f(x_2,a,g(z_2),y_2)$ et $f(x_2,a,g(z_2),y_2)\{x_2\mapsto x_1,y_2\mapsto y_1,z_2\mapsto z_1\}=f(x_1,a,g(z_1),y_1)$. Cependant, $f(x_1,a,g(z_1),y_1)$ n'est pas une variante de $f(x_2,a,g(x_2),x_2)$, car aucune substitution ne peut transformer ce dernier terme en le premier.$\{x_1\mapsto x_2,z_1\mapsto x_2,y_1\mapsto x_2\}$ réalise la direction inverse. Ce dernier terme est donc strictement plus spécial que le premier.

Une substitution $\sigma$ est plus spéciale que, ou subsumée par, une substitution $\tau$ si $x\sigma$ est plus spéciale que $x\tau$ pour chaque variable $x$. Par exemple, $\{x\mapsto f(u),y\mapsto f(f(u))\}$ est plus spécial que $\{x\mapsto z,y\mapsto f(z)\}$, puisque $f(u)$ et $f(f(u))$ est plus spécial que $z$ et $f(z)$, respectivement.

Anti-unification, généralisation

Un problème d'anti-unification est la donnée un couple $⟨t_1,t_2⟩$ de termes. Un term $t$ est une généralisation, ou anti-unificateur de $t_1$ et $t_2$ si $t{\sigma }_1\equiv t_1$ et $t{\sigma }_2\equiv t_2$ pour des substitutions ${\sigma }_1,{\sigma }_2$. Un ensemble $S$ d'anti-unificateurs est complet si toute généralisation subsume un terme $t\in S$; l'ensemble $S$ est minimal si aucun de ses membres ne subsume un autre.

Anti-unification syntaxique du premier ordre

L'anti-unification syntaxique du premier ordre est basée sur un ensemble de $T$ de termes du premier ordre (sur un ensemble donné $V$ de variables, $C$ de constantes et $F_n$ de symboles de fonctions $n$-aires), avec $\equiv$ étant lModèle:'égalité syntaxique. Dans ce cadre, chaque problème d'anti-unification $⟨t_1,t_2⟩$ possède un ensemble complet de solutions formé d'un singleton $\{t\}$. Son élément $t$ est appelé la plus petite généralisation du problème. Toute généralisation commune de $t_1$ et de $t_2$ subsume $t$. Cette plus petite généralisation est unique aux variantes près : si $S_1$ et $S_2$ sont tous deux des ensembles de solutions complets et minimaux du même problème syntaxique d'anti-unification, alors ils sont des singletons $S_1=\{s_1\}$ et $S_2=\{s_2\}$ pour certains termes $s_1$ et $s_2$, qui sont des renommages.

Gordon D. PlotkinModèle:, et John C. Reynolds ont donné un algorithme pour calculer la plus petite généralisation de deux termes donnés. Il présuppose une injection $\varphi :T\times T\to V$, c'est-à-dire une application attribuant à chaque paire $s,t$ de termes une variable distincte $\varphi (s,t)$. L'algorithme se compose de deux règles :

$f(s_1,\dots ,s_n)\bigsqcup f(t_1,\dots ,t_n)⇝f(s_1\bigsqcup t_1,\dots ,s_n\bigsqcup t_n)$

et

$s\bigsqcup t⇝\varphi (s,t)$

si la règle précédente n'est pas applicable.

Par exemple,

$(0*0)\bigsqcup (4*4)⇝(0\bigsqcup 4)*(0\bigsqcup 4)⇝\varphi (0,4)*\varphi (0,4)⇝x*x$.

Cette dernière généralisation représente le fait que les deux généralisations sont des nombres carrés.

Plotkin utilise son algorithme pour calculer la plus petite généralisation de deux ensembles de clauses en logique du premier ordre, ce qui est à la base de l'approche dite Modèle:Lien de la programmation logique inductive.

Anti-unification modulo une théorie

L'anti-unification modulo une théorie, aussi appelée anti-unification équationnelle, E-anti-unification, anti-unification dans une théorie est l'extension de l'anti-unification syntaxique dans les cas où les opérateurs sont assujettis à des axiomes, formant une théorie E. Généralement cette théorie est décrite par un ensemble d'égalités universelles. Par exemple, une théorie E peut contenir l'identité $u*v=v*u$ où les variables $u$ et $v$ sont implicitement quantifiées universellement et qui dit que l'opérateur $*$ est commutatif.

Des méthodes d'anti-unification ont été élaborées dans le cadre de termes sans rang avec des symboles de fonction d'arité non fixée et d'arbres.

Les termes sans rang diffèrent de ceux avec rang par le fait qu'ils n'ont pas d'arité fixe pour les symboles de fonction. Les haies (hedges) sont des séquences finies de tels termes. Ce sont des structures flexibles, utiles pour représenter des données semi-structurées. Pour tirer parti de la variabilité, les termes sans rang et leurs couvertures utilisent deux types de variables : les variables de terme, qui représentent un terme unique, et les variables de couverture, qui représentent des couvertures. Les techniques de résolution des termes sans rang et des couvertures ont été étudiés pour l'unification et de correspondance, puis pour l'anti-unification de ces structures par Kutsia Levy et Villaret.

Théories équationnelles

Il s'agit de théories avec des opérations ayant des propriétés particulières, typiquement des opérations associatives et commutatives, ou de théories commutatives ou l'emploi de grammaires, ou de théories plus complexes, ou des théories purement idempotentes.

Anti-unification nominale

L'anti-unification nominale consiste à calculer les généralisations minimales pour des termes dans un contexte donné. En général, le problème n'a pas de solution minimales, mais si l'ensemble des atomes autorisés dans les généralisations est fini, alors il existe une généralisation minimale qui est unique modulo modulo renommage et équivalence α. Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu ont donné un algorithme qui calcule la généralisation. L'algorithme s'appuie sur un sous-algorithme qui décide de manière constructive de l'équivalence de deux termes dans le contexte. L'anti-unification nominale peut être appliquée aux problèmes où la généralisation des termes du premier ordre est nécessaire (apprentissage inductif, détection de clones, etc.), mais où des liaisons sont impliquées

Applications

Des applications de l'anti-unification ont été faites en analyse des programmes, en factorisation de code source , en preuve inductive, en extraction d'information, en raisonnement par cas.

L'idée de généralisation de termes par rapport à une théorie équationnelle peut être retrouvée dans Manna et Waldinger qui en 1980 ont désiré l'appliquer à la synthèse de programmes

Anti-unification d'arbres et applications linguistiques

Les arbres syntaxiques pour des phrases peuvent être soumis à une généralisation minimale afin de dériver un arbres d'analyse maximal de sous-parties communes, dans le cadre de l'apprentissage des langues. Il y a des applications en fouille et classification de textes, ou des analyses de fourrés et d'autres opérations d'interaction entre les niveaux syntaxique et sémantique Modèle:,.

Bibliographie

Articles fondateurs

• Modèle:Article
• Modèle:Article
• Modèle:Article

Synthèses

• Modèle:Chapitre.
• Modèle:Chapitre.
• Modèle:Chapitre.

Articles

• Modèle:Article.
• Modèle:Article.
• Modèle:Article.
• Modèle:Chapitre
• Modèle:Article Software.
• Modèle:Chapitre

Articles liés

• Logique du premier ordre
• Lambda-calcul
• Unification