Mostrar código-fonte de Antiunificação (ciências da computação)

'''Antiunificação''' é o processo de construção de uma generalização comum a duas expressões simbólicas. Como na [[unificação]], várias '''estruturas''' são distinguidas dependendo de qual das expressões (também denominado termos) são permitidas e quais expressões são consideradas iguais. Se as variáveis que representam funções são permitidas em uma expressão, o processo é chamado de''' antiunificação de ordem superior''', caso contrário, de''' antiunificação de primeira ordem'''. Se a generalização requer a existência de uma instância literalmente igual para cada expressão de entrada, o processo é chamado de''' antiunificação sintática''', caso contrário, de''' E-antiunificação''', ou '''módulo da teoria da antiunificação'''.

Um [[algoritmo]] de antiunificação deve calcular, para expressões dadas, uma generalização '''completa '''e '''mínima '''de um conjunto, isto é, um conjunto, abrangendo todas as generalizações, e que não contenha membros redundantes, respectivamente. Dependendo da estrutura, uma generalização completa e mínima pode ter um, finitamente muitos, ou, possivelmente, um número infinito de membros, ou pode não existir;<ref group="note">Complete generalization sets always exist, but it may be the case that every complete generalization set is non-minimal.</ref> ela não pode ser vazia, uma vez que uma generalização trivial existe em qualquer caso. Para a antiunificação de primeira-ordem sintática, [[Gordon Plotkin]]<ref name="Plotkin.1970">{{citar periódico|primeiro1 =Gordon D.|último1 =Plotkin|título=A Note on Inductive Generalization|editor-nome1 =B.|editor-sobrenome1 =Meltzer|editor-nome2 =D.|editor-sobrenome2 =Michie|publicado=Edinburgh University Press|periódico=Machine Intelligence|volume=5|páginas=153–163|ano=1970}}</ref><ref name="Plotkin.1971">{{citar periódico|primeiro1 =Gordon D.|último1 =Plotkin|título=A Further Note on Inductive Generalization|editor-nome1 =B.|editor-sobrenome1 =Meltzer|editor-nome2 =D.|editor-sobrenome2 =Michie|publicado=Edinburgh University Press|periódico=Machine Intelligence|volume=6|páginas=101–124|ano=1971}}</ref> apresentou um algoritmo que calcula uma generalização completa e mínima de um conjunto unitário, o chamado '''menor''' '''generalização geral (mgg)'''.

Antiunificação não deve ser confundido com o [[desunificação]]. O segundo significa o processo de resolução de sistemas de[[Inequação|inequações]], que é de encontrar valores para as variáveis de tal forma que todas as inequações sejam satisfeitas.<ref group="note">Comon referred in 1986 to inequation-solving as "anti-unification", which nowadays has become quite unusual.</ref> Esta tarefa é bastante diferente da busca de generalizações.

== Pré-requisitos ==
Formalmente, uma abordagem de antiunificação pressupõe
* Um conjunto infinito ''V'' de '''variáveis'''. Para antiunificação de ordem superior, é conveniente escolher ''V'' disjunto do conjunto de [[Cálculo lambda|variáveis ligadas em termos lambda.]]
* Um conjunto ''T'' de '''termos''' tal que ''V'' ⊆ ''T''. Para antiunificação de primeira ordem ou de ordem superior, ''T'' é usualmente o conjunto de [[Termo (matemática)|termos de primeira ordem]] (termos construídos a partir de variáveis e símbolos de função) e [[Cálculo lambda|termos lambda]] (termos contendo variáveis de ordem superior), respectivamente.
* Uma [[relação de equivalência]] <math>\equiv</math> em <math>T</math>, indicando quais termos são considerados iguais. Para antiunificação de ordem superior, usualmente <math>t \equiv u</math> se <math>t</math> e <math>u</math> são [[Cálculo lambda|alpha equivalentes]]. Para primeira ordem E-antiunificação, <math>\equiv</math> reflete o conhecimento base sobre certos símbolos de função; por examplo, se <math>\oplus</math> é considerado comutativo, <math>t \equiv u</math> se <math>u</math> resulta de <math>t</math> trocando os argumentos de <math>\oplus</math> em algumas(possivelmente todas) ocorrências.<ref group="note">E.g. <math> a \oplus (b \oplus f(x)) \equiv a \oplus (f(x) \oplus b) \equiv (b \oplus f(x)) \oplus a \equiv (f(x) \oplus b) \oplus a</math></ref> Se não houver nenhum conhecimento base, então apenas literalmente, ou  sintaticamente, termos idênticos são considerados iguais.

=== Termo de primeira ordem ===
Dado um conjunto <math>V</math> de símbolos variáveis, um conjunto <math>C</math> de símbolos de constante e conjuntos <math>F_n</math> de símbolos de funções <math>n</math>-árias, também chamado de operador de símbolos, para cada número natural <math>n \geq 1</math> o conjunto de (não-ordenado de primeira ordem) termos <math>T</math> é [[Definição recursiva|definido recursivamente]] para ser o menor conjunto com as seguintes propriedades:<ref>{{citar livro|autor1 =C.C. Chang|autor2 =H. Jerome Keisler|título=Model Theory|ano=1977|volume=73|publicado=North Holland|editor1=A. Heyting|editor2=H.J. Keisler|editor3=A. Mostowski|editor4=A. Robinson|editor5=P. Suppes|series=Studies in Logic and the Foundation of Mathematics}}</ref>
* cada símbolo de variável é um termo: ''V'' ⊆ ''T'',
* cada símbolo de constante é um termo: ''C'' ⊆ ''T'',
* para todos os ''n'' termos ''t''<sub>1</sub>,...,''t<sub>n</sub>'', e a cada símbolo de função ''n''-ária ''f'' ∈ ''F<sub>n</sub>'', um termo maior pode ser construído.
Por exemplo, se ''x''&#x20;∈ ''V'' é um símbolo de variável, 1&#x20;∈ ''C'' é um símbolo de constante, e add&#x20;∈ ''F''<sub>2</sub> é um símbolo de função binária e, então, ''x''&#x20;∈ ''T'', 1&#x20;∈ ''T'', e (por isso) add(''x'',1)&#x20;∈ ''T'' pela primeira, segunda e terceira regra de construção do termo, respectivamente. O último termo é normalmente escrito como ''x''+1, usando [[notação infixa]] e o mais comum símbolo operador + por conveniência.

=== Termo de ordem superior ===
=== Substituição ===
Uma '''substituição '''é um mapeamento <math>\sigma: V \longrightarrow T</math> de variáveis para termos; a notação<math>\{x_1 \mapsto t_1, \ldots, x_k \mapsto t_k \}</math> se refere a uma substituição mapeando cada variável <math>x_i</math> para o termo <math>t_i</math>, para <math>i=1,\ldots,k</math>, e cada outra variável para ela mesma. '''Aplicando''' essa substitutição a um termo t é escrito em notação pós-fixa como <math>t \{x_1 \mapsto t_1, \ldots, x_k \mapsto t_k \}</math>; isso significa (simultaneamente) realocar cada ocorrência de cada variável <math>x_i</math> no termo t por <math>t_i</math>. O resultado tσ de aplicar uma substituição σ a um termo t é chamada uma '''instância''' daquele termo t.
Como um exemplo de primeira ordem, aplicando a substituição <math>\{x \mapsto h(a,y), z \mapsto b\}</math> ao termo
: {|
| {{Math|''f''(}}
| {{Math|''x''}}
| {{Math|, ''a'', ''g''(}}
| z
| {{Math|), ''y'')}}
| resulta em
|-
| {{Math|''f''(}}
| {{Math|''h''(''a'',''y'')}}
| {{Math|, ''a'', ''g''(}}
| b
| {{Math|), ''y'')}}
| .
|}

=== Generalização, especialização ===
Se um termo <math>t</math> possui uma instância equivalente a um termo <math>u</math>, isto é, se <math>t \sigma \equiv u</math> para alguma substituição <math>\sigma</math>, então <math>t</math> é chamado de '''mais geral '''que <math>u</math>, e <math>u</math> é chamado de '''mais especial '''que, ou '''subsumido''' por, <math>t</math>. Por exemplo, <math>x \oplus a</math> é mais geral que <math>a \oplus b</math> se <math>\oplus</math> é [[comutativo]], desde então <math>(x \oplus a)\{x \mapsto b\} = b \oplus a \equiv a \oplus b</math>.

Se <math>\equiv</math> é a identidade literal (sintática) dos termos, um termo pode ser tanto mais geral como mais especial que outro somente se ambos os termos diferem apenas nos nomes de suas variáveis, não em suas estruturas sintáticas; tais termos são chamados '''variantes''', ou '''renomeados''' de cada outro.
Por exemplo, <math>f(x_1,a,g(z_1),y_1)</math> é um variante <math>f(x_2,a,g(z_2),y_2)</math>, desde que <math>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)</math> e<math>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)</math>.
Contudo, <math>f(x_1,a,g(z_1),y_1)</math> ''não'' é um variante de <math>f(x_2,a,g(x_2),x_2)</math>, já que nenhuma substituição pode transformar o último termo no primeiro, embora <math>\{x_1 \mapsto x_2, z_1 \mapsto x_2, y_1 \mapsto x_2 \}</math> atinge a direção inversa.
O último termo é, portanto, mais especial do que o anterior.

Uma substituição <math>\sigma</math> é '''mais especial''' que, ou '''subsumida''' por, uma substituição <math>\tau</math> se <math>x \sigma</math> é mais especial que <math>x \tau</math> para cada variável <math>x</math>.
Por exemplo, <math>\{ x \mapsto f(u), y \mapsto f(f(u)) \}</math> é mais especial <math>\{ x \mapsto z, y \mapsto f(z) \}</math>, desde que <math>f(u)</math> e <math>f(f(u)) </math> seam mais especiais que <math>z</math> e <math>f(z)</math>, respectivamente.

=== Problema de antiunificação, conjunto de generalização ===
Um '''problema de antiunificação '''é um par <math>\langle t_1, t_2 \rangle</math> de termos.
Um termo <math>t</math> é uma '''generalização '''comum, ou '''antiunificador''', de <math>t_1</math> e <math>t_2</math> se <math>t \sigma_1 \equiv t_1</math> e <math>t \sigma_2 \equiv t_2</math> para alguma substituição <math>\sigma_1, \sigma_2</math>.
Para um dado  problema de antiunificação, um conjunto <math>S</math> de antiunificadores é chamado '''completo''' se cada generalização subsume algum termo <math>t \in S</math>; o conjunto <math>S</math> é chamado '''mínimo''' se nenhum de seus membros subsume outro.

== Antiunificação sintática de primeira ordem ==
A estrutura de antiunificação sintática de primeira ordem é baseada em <math>T</math> sendo o conjunto de ''termos de primeira ordem'' (sobre dado algum conjunto <math>V</math> de variáveis, <math>C</math> de constantes e <math>F_n</math> de símbolos de função <math>n</math>-ária) e em <math>\equiv</math> sendo ''igualdade sintática''.
Nesta estrutura, cada problema de antiunificação <math>\langle t_1, t_2 \rangle</math> tem uma completo, e obviamente mínimo, [[conjunto unitário]] solução <math>\{t\}</math>.
Seu membro <math>t</math> é chamado de '''menor generalização geral (mgg)''' do problema, ele tem uma instância sintaticamente igual a <math>t_1</math> e uma outra sintaticamente igual a <math>t_2</math>.
Qualquer generalização comum de <math>t_1</math> e <math>t_2</math> subsume <math>t</math>.
O mgg é único para cada variante: se <math>S_1</math> e <math>S_2</math> são ambos conjuntos solução completos e mínimos do mesmo problema de antiunificação sintática, então <math>S_1 = \{ s_1\}</math> e <math>S_2 = \{ s_2 \}</math> para algum termo <math>s_1</math> e <math>s_2</math>, que são[[Termo (matemática)|renomeados]] de cada outro.

Plotkin<ref name="Plotkin.1970"/><ref name="Plotkin.1971"/> tem dado um algoritmo para computar o lgg de dois termos dados.
Isso pressupõe um [[Função injectiva|mapeamento injetivo]] <math>\phi: T \times T \longrightarrow V</math>, isto é, um mapeamento atribuindo cada par <math>s,t</math> de termos uma própria variável <math>\phi(s,t)</math>, tal que dois pares não compartilham da mesma variável.
<ref group="note">From a theoretical viewpoint, such a mapping exists, since both <math>V</math> and  <math>T \times T</math> are [//en.wikipedia.org/wiki/Countably_infinite countably infinite] sets; for practical purposes, <math>\phi</math> can be built up as needed, remembering assigned mappings <math>\langle s,t,\phi(s,t) \rangle</math> in a [//en.wikipedia.org/wiki/Hash_table hash table].</ref>
O algoritmo consiste em duas regras: 
: {|
| align="right" | <math> f(s_1,\dots,s_n) \sqcup f(t_1,\ldots,t_n) </math>
| <math> \rightsquigarrow </math>
| <math> f( s_1 \sqcup t_1,  \ldots, s_n \sqcup t_n ) </math>
|-
| align="right" | <math> s \sqcup t </math>
| <math> \rightsquigarrow </math>
| <math> \phi(s,t) </math>
| align="right" | se a regra anterior não for aplicável
|}
Por exemplo, <math>(0*0) \sqcup (4*4) \rightsquigarrow (0 \sqcup 4)*(0 \sqcup 4) \rightsquigarrow \phi(0,4) * \phi(0,4) \rightsquigarrow x*x</math>; esta menor generalização geral reflete a propriedade comum de ambas entradas serem números quadrados.

Plotkin usou seu algoritmo para computar o "[[Inductive logic programming#Example|menor generalização geral relativa (mggr)]]" de dois conjuntos de cláusulas na [[lógica de primeira ordem]], que foi a base da abordagem [[Golem (ILP)|Golem]] para [[programação da lógica indutiva|programação de lógica indutiva]].

== Módulo da teoria da antiunificação de primeira ordem ==
* {{Citation|título=Unification and Anti-Unification|último1 =Jacobson|primeiro1 =Erik|data=junho de 1991|series=Technical Report}}
* {{Citation|título=A Functional Reconstruction of Anti-Unification|último1 =Østvold|primeiro1 =Bjarte M.|data=abril de 2004|series=NR Note|volume=DART/04/04|publicado=Norwegian Computing Center}}
* Boytcheva, Svetla; Markov, Zdravko (2002). "An Algorithm for Inducing Least Generalization Under Relative Implication".
* Kutsia, Temur; Levy, Jordi; Villaret, Mateu (2014). "[http://link.springer.com/content/pdf/10.1007%2Fs10817-013-9285-6.pdf Anti-Unification for Unranked Terms and Hedges]" (PDF). Journal of Automated Reasoning. Springer. 52 (2): 155–190. [[Digital object identifier|doi]]:[[doi:10.1007/s10817-013-9285-6|10.1007/s10817-013-9285-6]]. [http://www.risc.jku.at/projects/stout/software/antiunify.php Software].

=== Teorias equacionais ===
* Uma operação associativa e comutativa: {{Citation|título=Algorithms des completion et generalisation en logic du premier ordre|último1 =Pottier|primeiro1 =Loic|data=fevereiro de 1989}}; {{Citation|título=Generalisation de termes en theorie equationelle – Cas associatif-commutatif|ano=1989|último1 =Pottier|primeiro1 =Loic|series=INRIA Report|volume=1056|publicado=INRIA}}
* Teoria comutativa: [[Franz Baader]] (1991). "Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems". Proc. 4th Conf. on Rewriting Techniques and Applications (RTA). LNCS.''' 488'''. Springer. pp.&nbsp;86–91.<span title="ctx_ver=Z39.88-2004&rfr_id=info%3Asid%2Fpt.wikipedia.org%3AMain+Page&rft.genre=conference&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook" class="Z3988" id="cxmwAR8" tabindex="0">&nbsp;</span>
* Monóides livres: {{Citation|título=Normalisierung, Unifikation und Antiunifikation in Freien Monoiden|ano=1993|último1 =Biere|primeiro1 =A.|url=http://fmv.jku.at/papers/Biere-Diploma-Thesis-1993.pdf|publicado=Univ. Karlsruhe, Germany}}
* Classes regulares de congruência: {{Citation|título=Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung|último1 =Heinz|primeiro1 =Birgit|data=dezembro de 1995|series=GMD Berichte|volume=261|publicado=TU Berlin6|isbn=3-486-23873-6}}; Burghardt, Jochen (2005). "[http://user.cs.tu-berlin.de/~jochen/aij05.pdf E-Generalization Using Grammars]{{Ligação inativa|1=data=junho de 2019 }}" (PDF). ''Artificial Intelligence Journal''. [[Elsevier]]. '''165''' (1): 1–35. [[Digital object identifier|doi]]:[[doi:10.1016/j.artint.2005.01.008|10.1016/j.artint.2005.01.008.]]<span style="color: #0645ad;"> </span>
* A-, C-, AC-, ACU- Teorias com tipos ordenados: Alpuente, Maria; Escobar, Santiago; Espert, Javier; Meseguer, Jose (2014). "[https://www.ideals.illinois.edu/bitstream/handle/2142/25871/journal.pdf A modular order-sorted equational generalization algorithm]" (PDF). Information and Computation. Elsevier. '''235''': 98–136. [[doi]]:[[doi:10.1016/j.ic.2014.01.006|10.1016/j.ic.2014.01.006.]]

=== Antiunificação ordenada de primeira ordem ===
* Tipos taxonômicos: Frisch, Alan M.; Page, David (1990). "Generalisation with Taxonomic Information". AAAI: 755–761.; Frisch, Alan M.; Page Jr., C. David (1991). "Generalizing Atoms in Constraint Logic". ''Proc. Conf. on Knowledge Representation''.; Frisch, A.M.; Page, C.D. (1995). "Building Theories into Instantiation". In Mellish, C.S. ''Proc. 14th IJCAI''. Morgan Kaufmann. pp.&nbsp;1210–1216.
* Termos de destaque: Plaza, E. (1995). "Cases as Terms: A Feature Term Approach to the Structured Representation of Cases". ''Proc. 1st International Conference on Case-Based Reasoning (ICCBR)''. LNCS. '''1010'''. Springer. pp.&nbsp;265–276. [[ISSN]] [https://www.worldcat.org/issn/0302-9743 0302-9743.]
* Idestam-Almquist, Peter (Jun 1993). "Generalization under Implication by Recursive Anti-Unification".'' Proc. 10th Conf. on Machine Learning''. Morgan Kaufmann. pp.&nbsp;151–158.
* Fischer, Cornelia (May 1994), ''PAntUDE – An Anti-Unification Algorithm for Expressing Refined Generalizations'', Research Report, TM-94-04, DFKI
* A-, C-, AC-, ACU-theories with ordered sorts: [[#Teorias equacionais|ver acima]]

=== Antiunificação nominal ===
* Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (Jun 2013). [http://drops.dagstuhl.de/opus/volltexte/2015/5189/pdf/9.pdf Nominal Anti-Unification]. Proc. RTA 2015. Vol. 36 of LIPIcs. Schloss Dagstuhl, 57-73. [http://www.risc.jku.at/projects/stout/software/nau.php Software.]

=== Aplicações ===
* Análise do programa: Bulychev, Peter; Minea, Marius (2008). "Duplicate Code Detection Using Anti-Unification".; Bulychev, Peter E.; Kostylev, Egor V.; Zakharov, Vladimir A. (2009). "Anti-Unification Algorithms and their Applications in Program Analysis".
* Fatoração de código: Cottrell, Rylan (Sep 2008), ''Semi-automating Small-Scale Source Code Reuse via Structural Correspondence'', Univ. Calgary
* Prova indutiva: Heinz, Birgit (1994), ''Lemma Discovery by Anti-Unification of Regular Sorts'', Technical Report, 94-21, TU Berlin
* Extração de informação: Thomas, Bernd (1999). "Anti-Unification Based Learning of T-Wrappers for Information Extraction". ''AAAI Technical Report''. WS-99-11: 15–20.
* Raciocínio baseado em casos: Armengol, Eva; Plaza, Enric (2005). "Using Symbolic Descriptions to Explain Similarity on CBR".

=== Antiunificação de árvores e aplicações linguísticas ===
* Árvores sintáticas para sentenças podem ser sujeitas a menor generalização geral para derivar uma subárvore sintática máxima comum para aprendizado de línguas. Existem aplicações em busca e classificação de texto.<ref>Boris Galitsky; Josep Lluís de la Rose; Gabor Dobrocsi (2011). "Mapping Syntactic to Semantic Generalizations of Linguistic Parse Trees". ''FLAIRS Conference''.</ref>
* Florestas sintáticas para parágrafos como grafos podem ser sujeitas a menor generalização geral.<ref>Boris Galitsky; Kuznetsov SO; Usikov DA (2013). "Parse Thicket Representation for Multi-sentence Search". ''Lecture Notes in Computer Science''. '''7735''': 1072–1091. [[Digital object identifier|doi]]:[[doi:10.1007/978-3-642-35786-2 12|10.1007/978-3-642-35786-2_12]]</ref>
* Operação de generalização comuta com a operação de transição de um nível sintático (árvores sintáticas) a um semântico (expressões simbólicas). O último pode ser sujeito à antiunificação convencional.<ref>Boris Galitsky; Gabor Dobrocsi; Josep Lluís de la Rosa; Sergei O. Kuznetsov (2010). [http://link.springer.com/chapter/10.1007%2F978-3-642-14197-3_19 "From Generalization of Syntactic Parse Trees to Conceptual Graphs"]. ''Lecture Notes in Computer Science''. '''6208''': 185–190. [[Digital object identifier|doi]]:[[doi:10.1007/978-3-642-14197-3 19|10.1007/978-3-642-14197-3_19]]</ref><ref>Boris Galitsky; de la Rosa JL; Dobrocsi G. (2012). "Inferring the semantic properties of sentences by mining syntactic parse trees". ''Data & Knowledge Engineering''. 81-82: 21–45. doi:[[doi:10.1016/j.datak.2012.07.003|10.1016/j.datak.2012.07.003]].</ref>

== Antiunificação de ordem superior ==
* Cálculos de construções: [[Frank Pfenning]] (Jul 1991). "[http://www.cs.cmu.edu/~fp/papers/lics91.pdf Unification and Anti-Unification in the Calculus of Constructions]" (PDF). ''Proc. 6th LIC''S. Springer. pp.&nbsp;74–85.<span title="ctx_ver=Z39.88-2004&rfr_id=info%3Asid%2Fpt.wikipedia.org%3AMain+Page&rft.genre=conference&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook" class="Z3988" id="cxmwAV0" tabindex="0">&nbsp;</span>
* Cálculo lambda simplesmente digitado (Entrada: Termos na eta-longa beta-normal forma. Saída:  padrões de ordem superior): Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (Jun 2013). [http://drops.dagstuhl.de/opus/volltexte/2013/4057/pdf/10.pdf A Variant of Higher-Order Anti-Unification]. Proc. RTA 2013. Vol. 21 of LIPIcs. Schloss Dagstuhl, 113-127. [http://www.risc.jku.at/projects/stout/software/hoau.php Software.]
* Substituições restritas de ordem superior:  {{Citation|título=Combinatorically Restricted Higher Order Anti-Unification|último1 =Wagner|primeiro1 =Ulrich|data=abril de 2002|publicado=TU Berlin}}; {{Citation|título=Restricted Higher-Order Anti-Unification for Heuristic-Driven Theory Projection|último1 =Schmidt|primeiro1 =Martin|data=setembro de 2010|url=http://ikw.uni-osnabrueck.de/de/system/files/31-2010.pdf|series=PICS-Report|volume=31-2010|publicado=Univ. Osnabrück, Germany|issn=1610-5389}}

== Notas ==
{{Referências|grupo=note}}

{{Referências}}

[[Categoria:Lógica matemática]]