Anti-unification

En informatique théorique et en logique mathématique, l'anti-unification est la construction d'une généralisation commune à deux termes symboliques données. Comme son nom l’indique, c'est l'opération duale^[é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'$ de $t_{1}$ et $t_{2}$, il existe une substitution $\xi$ telle qui $t=t'\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 dual^[é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 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 disunification (en). Cette dernière consiste à résoudre des systèmes de « diséquations » (c'est-à-dire de la forme $e\neq e'$), 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 $\langle t_{1},t_{2}\rangle$ 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 l'égalité syntaxique. Dans ce cadre, chaque problème d'anti-unification $\langle t_{1},t_{2}\rangle$ 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. 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 $\phi :T\times T\to V$, c'est-à-dire une application attribuant à chaque paire $s,t$ de termes une variable distincte $\phi (s,t)$. L'algorithme se compose de deux règles :

$f(s_{1},\dots ,s_{n})\sqcup f(t_{1},\ldots ,t_{n})\rightsquigarrow f(s_{1}\sqcup t_{1},\ldots ,s_{n}\sqcup t_{n})$

et

$s\sqcup t\rightsquigarrow \phi (s,t)$

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

Par exemple,

$(0*0)\sqcup (4*4)\rightsquigarrow (0\sqcup 4)*(0\sqcup 4)\rightsquigarrow \phi (0,4)*\phi (0,4)\rightsquigarrow 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 Golem (en) 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 .

Bibliographie

Articles fondateurs

• Gordon D. Plotkin, « A Note on Inductive Generalization », Machine Intelligence, vol. 5, n^o 1,‎ 1970, p. 153–163 (lire en ligne)
• John C. Reynolds, « Transformational systems and the algebraic structure of atomic formulas », Machine Intelligence, vol. 5, n^o 1,‎ 1970, p. 135–151 (lire en ligne)
• Gordon D. Plotkin, « A Further Note on Inductive Generalization », Machine Intelligence, vol. 6,‎ 1971, p. 101–124

Synthèses

• F. Baader et W. Snyder, « Unification theory », dans John Alan Robinson et Andrei Voronkov (éditeurs), Handbook of Automated Reasoning, vol. 1, Elsevier, 2001, 2122 p. (lire en ligne), p. 447-533.
• Alexander Baumgartner et Temur Kutsia, « A Library of Anti-unification Algorithms », dans E. Fermé E. et J. Leite (éditeurs), Logics in Artificial Intelligence. JELIA 2014, Springer Cham, coll. « Lecture Notes in Computer Science » (n^o 8761), 2014 (DOI 10.1007/978-3-319-11558-0_38, présentation en ligne), p. 543–557.
• Peter E. Bulychev, Egor V. Kostylev et Vladimir A. Zakharov, « Anti-unification Algorithms and Their Applications in Program Analysis », dans A. Pnueli, I. Virbitskaite et A. Voronkov (éditeurs), Perspectives of Systems Informatics. PSI 2009, Springer, coll. « Lecture Notes in Computer Science » (n^o 5947), 2010 (DOI 10.1007/978-3-642-11486-1_35, présentation en ligne), p. 413–423.

Articles

• Gonzague Yernaux et Wim Vanhoof, « Anti-unification in Constraint Logic Programming », Theory and Practice of Logic Programming, vol. 19, n^os 5-6 (35th International Conference on Logic Programming),‎ 2019, p. 773-789 (DOI 10.1017/S1471068419000188).
• David M. Cerna, « Anti-unification and the theory of semirings », Theoretical Computer Science, vol. 848,‎ 2020, p. 133–139 (DOI 10.1016/j.tcs.2020.10.020).
• Adam D. Barwell, Christopher Brown et Kevin Hammond, « Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification », Future Generation Computer Systems, vol. 79,‎ 2018, p. 669–686 (DOI 10.1016/j.future.2017.07.024).
• David M. Cerna et Temur Kutsia, « A Generic Framework for Higher-Order Generalizations », dans Herman Geuvers (éditeur), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, coll. « Leibniz International Proceedings in Informatics (LIPIcs) » (n^o 131), 2019 (DOI 10.4230/LIPIcs.FSCD.2019.10, lire en ligne), p. 10:1-10:19
• Temur Kutsia, Jordi Levy et Mateu Villaret, « Anti-Unification for Unranked Terms and Hedges », Journal of Automated Reasoning, vol. 52, n^o 2,‎ 2014, p. 155–190 (DOI 10.1007/s10817-013-9285-6, lire en ligne) Software.
• Alexander Baumgartner, Temur Kutsia, Jordi Levy et Mateu Villaret, « Nominal Anti-Unification », dans Proc. RTA 2015, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, coll. « Leibniz International Proceedings in Informatics (LIPIcs) » (n^o 36), 2015 (DOI 10.4230/LIPIcs.RTA.2015.57, lire en ligne), p. 57-73

Articles liés

• Logique du premier ordre
• Lambda-calcul
• Unification