Anti-unification

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 ${\displaystyle \equiv }$ sur ${\displaystyle T}$, indiquant quels termes sont considérés comme égaux. Pour l'unification d'ordre supérieur, on a ${\displaystyle t\equiv u}$ si ${\displaystyle t}$ et ${\displaystyle u}$ sont alpha equivalents. Pour le premier ordre, ${\displaystyle \equiv }$ représente une certaine connaissance sur les symboles de fonction ; si par exemple ${\displaystyle \oplus }$ est commutative, on a ${\displaystyle t\equiv u}$ si ${\displaystyle u}$ et ${\displaystyle t}$ sont les mêmes par échange d'arguments de ${\displaystyle \oplus }$ dans certaines ou toutes les occurrences[note 2]. Si aucune information n'est disponible, l'équivalence se réduit à l'égalité.

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

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

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

Si ${\displaystyle \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, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ est une variante de ${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$, puisque ${\displaystyle 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 ${\displaystyle 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, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ n'est pas une variante de ${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$, car aucune substitution ne peut transformer ce dernier terme en le premier.${\displaystyle \{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 ${\displaystyle \sigma }$ est plus spéciale que, ou subsumée par, une substitution ${\displaystyle \tau }$ si ${\displaystyle x\sigma }$ est plus spéciale que ${\displaystyle x\tau }$ pour chaque variable ${\displaystyle x}$. Par exemple, ${\displaystyle \{x\mapsto f(u),y\mapsto f(f(u))\}}$ est plus spécial que ${\displaystyle \{x\mapsto z,y\mapsto f(z)\}}$, puisque ${\displaystyle f(u)}$ et ${\displaystyle f(f(u))}$ est plus spécial que ${\displaystyle z}$ et ${\displaystyle f(z)}$, respectivement.

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

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[7] ou l'emploi de grammaires[8], ou de théories plus complexes[9], ou des théories purement idempotentes[10].

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[11]

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[18], ou des analyses de fourrés[19] et d'autres opérations d'interaction entre les niveaux syntaxique et sémantique [20]^,[21].