Anti-unification
En informatique théorique et en logique mathématique, lanti-unification est la construction d'une généralisation commune à deux termes symboliques données. Comme son nom l’indique, c'est l' 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  est une généralisation de deux termes  et  si  et , pour des substitutions  et  . Une généralisation  de  et  est minimale, ou la plus spécifique, si pour toute généralisation   de  et , il existe une substitution  telle qui . 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  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 Plotkin 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 . Cette dernière consiste à résoudre des systèmes de « diséquations » (c'est-à-dire de la forme ), 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  sur , indiquant quels termes sont considérés comme égaux. Pour l'unification d'ordre supérieur, on a  si  et  sont alpha equivalents. Pour le premier ordre,  représente une certaine connaissance sur les symboles de fonction ; si par exemple   est commutative, on a  si  et   sont les mêmes par échange d'arguments de  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   des variables dans des termes ; le résultat de l'application d'une substitution  à un terme  est appelé une instance de .

Par exemple, l'application de la substitution  au terme   produit .

Généralisation et spécialisation 

Si un terme  a une instance qui est équivalente à un terme , c'est-à-dire si  pour une substitution , alors  est dit plus général que , et  est appelé plus particulier que . Par exemple,  est plus général que  si  est commutative, puisque.

Si  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,  est une variante de , puisque  et .
Cependant,  n'est pas une variante de , car aucune substitution ne peut transformer ce dernier terme en le premier. réalise la direction inverse.
Ce dernier terme est donc strictement plus spécial que le premier.

Une substitution  est plus spéciale que, ou subsumée par, une substitution  si  est plus spéciale que  pour chaque variable . Par exemple,  est plus spécial que , puisque  et  est plus spécial que  et , respectivement.

Anti-unification, généralisation 

Un problème d'anti-unification est la donnée un couple  de termes.
Un term  est une généralisation, ou anti-unificateur de  et  si  et  pour des substitutions .
Un ensemble  d'anti-unificateurs est complet si toute généralisation subsume un terme ; l'ensemble  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  de termes du premier ordre (sur un ensemble donné  de variables,  de constantes et  de symboles de fonctions -aires), avec  étant légalité syntaxique.
Dans ce cadre, chaque problème d'anti-unification  possède un ensemble complet de solutions formé d'un singleton . Son élément  est appelé la plus petite généralisation du problème. Toute généralisation commune de  et de  subsume .
Cette plus petite généralisation est unique aux variantes près : si  et  sont tous deux des ensembles de solutions complets et minimaux du même problème syntaxique d'anti-unification, alors ils sont des singletons  et  pour certains termes  et , qui sont des renommages.

Gordon D. Plotkin 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 , c'est-à-dire une application attribuant à chaque paire  de termes une variable distincte . L'algorithme se compose de deux règles :

et

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

Par exemple,
.
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  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é  où les variables  et  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
.

Notes

Références

Bibliographie 

Articles fondateurs
 
 
 

Synthèses
 .
 .
 .

Articles
.
.
.

 Software.

Articles liés 
 Logique du premier ordre
 Lambda-calcul
 Unification

Programmation informatique
Logique
Algèbre
Informatique théorique
Logique mathématique
Réécriture
Syntaxe
Langage de programmation logique