Anti-unification
![Page d’aide sur l’homonymie](http://upload.wikimedia.org/wikipedia/commons/thumb/6/6f/Confusion_colour.svg/20px-Confusion_colour.svg.png)
Ne doit pas être confondu avec disunification.
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 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 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[note 1] ; 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[1],[2] 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 ), 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[note 2]. 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[3],[4] et John C. Reynolds[5] 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 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é 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[6].
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[6].
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[7] ou l'emploi de grammaires[8], ou de théories plus complexes[9], ou des théories purement idempotentes[10].
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[11]
Applications
Des applications de l'anti-unification ont été faites en analyse des programmes[12], en factorisation de code source [13], en preuve inductive[14], en extraction d'information[15], en raisonnement par cas[16].
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[17]
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[18], ou des analyses de fourrés[19] et d'autres opérations d'interaction entre les niveaux syntaxique et sémantique [20],[21].
Notes
Références
- ↑ Gordon D. Plotkin, « A Note on Inductive Generalization », Machine Intelligence, vol. 5, , p. 153–163
- ↑ Gordon D. Plotkin, « A Further Note on Inductive Generalization », Machine Intelligence, vol. 6, , p. 101–124
- ↑ Plotkin 1970.
- ↑ Plotkin 1971.
- ↑ Reynolds 1970.
- ↑ a et b Kutsia, Levy et Villaret 2014.
- ↑ Franz Baader, « Unification, weak unification, upper bound, lower bound, and generalization problems », Lecture Notes in Computer Science, vol. 488 « Proc. 4th Conf. on Rewriting Techniques and Applications (RTA) », , p. 86-97 (ISSN 0302-9743, DOI 10.1007/3-540-53904-2_88).
- ↑ Jochen Burghardt, « E-Generalization Using Grammars », Artificial Intelligence, vol. 165, no 1, , p. 1–35 (DOI 10.1016/j.artint.2005.01.008, arXiv 1403.8118).
- ↑ Maria Alpuente, Santiago Escobar, Javier Espert et Jose Meseguer, « A modular order-sorted equational generalization algorithm », Information and Computation, vol. 235, , p. 98–136 (DOI 10.1016/j.ic.2014.01.006, hdl 2142/25871, lire en ligne).
- ↑ David Cerna et Temur Kutsia, « Idempotent Anti-Unification », ACM Transactions in Computational Logic, vol. 21, no 2, (hdl 10.1145/3359060, lire en ligne).
- ↑ Baumgartner et al. 2015.
- ↑ Bulychev, Kostylev et Zakharov 2009.
- ↑ Rylan Cottrell, Robert J. Walker et Jörg Denzinger, « Semi-automating small-scale source code reuse via structural correspondence », SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, , p. 214-225 (DOI 10.1145/1453101.1453130)
- ↑ Birgit Heinz, « Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung », GMD-Bericht, vol. 261, (ISBN 978-3-486-23873-0)
- ↑ Bernd Thomas, « Anti-Unification Based Learning of T-Wrappers for Information Extraction », AAAI Technical Report, vol. WS-99-11, , p. 15–20
- ↑ Eva Armengol et Enric Plaza, « Using Symbolic Descriptions to Explain Similarity on CBR », nternational Conference of the Catalan Association for Artificial Intelligence, , p. 239-246
- ↑ Zohar Manna and Richard Waldinger, « A Deductive Approach to Program Synthesis », ACM Transactions on Programming Languages and Systems, vol. 2, , p. 90–121 (DOI 10.1145/357084.357090).
- ↑ Boris Galitsky, Josep Lluís de la Rose et Gabor Dobrocsi, « Mapping Syntactic to Semantic Generalizations of Linguistic Parse Trees », FLAIRS Conference, .
- ↑ Boris Galitsky, Kuznetsov SO et Usikov DA, « Parse Thicket Representation for Multi-sentence Search », Lecture Notes in Computer Science, vol. 7735, , p. 1072–1091 (ISBN 978-3-642-35785-5, DOI 10.1007/978-3-642-35786-2_12).
- ↑ Boris Galitsky, Gabor Dobrocsi, Josep Lluís de la Rosa et Sergei O. Kuznetsov, « From Generalization of Syntactic Parse Trees to Conceptual Graphs », Lecture Notes in Computer Science, vol. 6208, , p. 185–190 (ISBN 978-3-642-14196-6, DOI 10.1007/978-3-642-14197-3_19)
- ↑ Boris Galitsky, de la Rosa JL et Dobrocsi G., « Inferring the semantic properties of sentences by mining syntactic parse trees », Data & Knowledge Engineering, vol. 81-82, , p. 21–45 (DOI 10.1016/j.datak.2012.07.003)
Bibliographie
- Articles fondateurs
- Gordon D. Plotkin, « A Note on Inductive Generalization », Machine Intelligence, vol. 5, no 1, , p. 153–163 (lire en ligne)
- John C. Reynolds, « Transformational systems and the algebraic structure of atomic formulas », Machine Intelligence, vol. 5, no 1, , p. 135–151 (lire en ligne)
- Gordon D. Plotkin, « A Further Note on Inductive Generalization », Machine Intelligence, vol. 6, , 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, , 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 » (no 8761), (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 » (no 5947), (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, nos 5-6 (35th International Conference on Logic Programming), , p. 773-789 (DOI 10.1017/S1471068419000188).
- David M. Cerna, « Anti-unification and the theory of semirings », Theoretical Computer Science, vol. 848, , 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, , 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) » (no 131), (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, no 2, , 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) » (no 36), (DOI 10.4230/LIPIcs.RTA.2015.57, lire en ligne), p. 57-73
Articles liés
Portail de la logique
Portail de l’informatique
Portail de l'informatique théorique