Abrir menu principal

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;[note 1] 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[1][2] 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 deinequações, que é de encontrar valores para as variáveis de tal forma que todas as inequações sejam satisfeitas.[note 2] Esta tarefa é bastante diferente da busca de generalizações.

Pré-requisitosEditar

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 variáveis ligadas em termos lambda.
  • Um conjunto T de termos tal que VT. Para antiunificação de primeira ordem ou de ordem superior, T é usualmente o conjunto de termos de primeira ordem (termos construídos a partir de variáveis e símbolos de função) e termos lambda (termos contendo variáveis de ordem superior), respectivamente.
  • Uma relação de equivalência   em  , indicando quais termos são considerados iguais. Para antiunificação de ordem superior, usualmente   se   e   são alpha equivalentes. Para primeira ordem E-antiunificação,   reflete o conhecimento base sobre certos símbolos de função; por examplo, se   é considerado comutativo,   se   resulta de   trocando os argumentos de   em algumas(possivelmente todas) ocorrências.[note 3] Se não houver nenhum conhecimento base, então apenas literalmente, ou sintaticamente, termos idênticos são considerados iguais.

Termo de primeira ordemEditar

Dado um conjunto   de símbolos variáveis, um conjunto   de símbolos de constante e conjuntos   de símbolos de funções  -árias, também chamado de operador de símbolos, para cada número natural   o conjunto de (não-ordenado de primeira ordem) termos   é definido recursivamente para ser o menor conjunto com as seguintes propriedades:[3]

  • cada símbolo de variável é um termo: VT,
  • cada símbolo de constante é um termo: CT,
  • para todos os n termos t1,...,tn, e a cada símbolo de função n-ária fFn, um termo maior pode ser construído.

Por exemplo, se xV é um símbolo de variável, 1 ∈ C é um símbolo de constante, e add ∈ F2 é um símbolo de função binária e, então, xT, 1 ∈ T, e (por isso) add(x,1) ∈ 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 superiorEditar

SubstituiçãoEditar

Uma substituição é um mapeamento   de variáveis para termos; a notação  se refere a uma substituição mapeando cada variável   para o termo  , para  , e cada outra variável para ela mesma. Aplicando essa substitutição a um termo t é escrito em notação pós-fixa como  ; isso significa (simultaneamente) realocar cada ocorrência de cada variável   no termo t por  . 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   ao termo

f( x , a, g( z ), y) resulta em
f( h(a,y) , a, g( b ), y) .

Generalização, especializaçãoEditar

Se um termo   possui uma instância equivalente a um termo  , isto é, se   para alguma substituição  , então   é chamado de mais geral que  , e   é chamado de mais especial que, ou subsumido por,  . Por exemplo,   é mais geral que   se   é comutativo, desde então  .

Se   é 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,   é um variante  , desde que   e . Contudo,   não é um variante de  , já que nenhuma substituição pode transformar o último termo no primeiro, embora   atinge a direção inversa. O último termo é, portanto, mais especial do que o anterior.

Uma substituição   é mais especial que, ou subsumida por, uma substituição   se   é mais especial que   para cada variável  . Por exemplo,   é mais especial  , desde que   e   seam mais especiais que   e  , respectivamente.

Problema de antiunificação, conjunto de generalizaçãoEditar

Um problema de antiunificação é um par   de termos. Um termo   é uma generalização comum, ou antiunificador, de   e   se   e   para alguma substituição  . Para um dado  problema de antiunificação, um conjunto   de antiunificadores é chamado completo se cada generalização subsume algum termo  ; o conjunto   é chamado mínimo se nenhum de seus membros subsume outro.

Antiunificação sintática de primeira ordemEditar

A estrutura de antiunificação sintática de primeira ordem é baseada em   sendo o conjunto de termos de primeira ordem (sobre dado algum conjunto   de variáveis,   de constantes e   de símbolos de função  -ária) e em   sendo igualdade sintática. Nesta estrutura, cada problema de antiunificação   tem uma completo, e obviamente mínimo, conjunto unitário solução  . Seu membro   é chamado de menor generalização geral (mgg) do problema, ele tem uma instância sintaticamente igual a   e uma outra sintaticamente igual a  . Qualquer generalização comum de   e   subsume  . O mgg é único para cada variante: se   e   são ambos conjuntos solução completos e mínimos do mesmo problema de antiunificação sintática, então   e   para algum termo   e  , que sãorenomeados de cada outro.

Plotkin[1][2] tem dado um algoritmo para computar o lgg de dois termos dados. Isso pressupõe um mapeamento injetivo  , isto é, um mapeamento atribuindo cada par   de termos uma própria variável  , tal que dois pares não compartilham da mesma variável. [note 4] O algoritmo consiste em duas regras: 

     
      se a regra anterior não for aplicável

Por exemplo,  ; esta menor generalização geral reflete a propriedade comum de ambas entradas serem números quadrados.

Plotkin usou seu algoritmo para computar o "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 para programação de lógica indutiva.

Módulo da teoria da antiunificação de primeira ordemEditar

  • Jacobson, Erik (junho de 1991), Unification and Anti-Unification, Technical Report 
  • Østvold, Bjarte M. (abril de 2004), A Functional Reconstruction of Anti-Unification, NR Note, DART/04/04, Norwegian Computing Center 
  • Boytcheva, Svetla; Markov, Zdravko (2002). "An Algorithm for Inducing Least Generalization Under Relative Implication".
  • Kutsia, Temur; Levy, Jordi; Villaret, Mateu (2014). "Anti-Unification for Unranked Terms and Hedges" (PDF). Journal of Automated Reasoning. Springer. 52 (2): 155–190. doi:10.1007/s10817-013-9285-6. Software.

Teorias equacionaisEditar

Antiunificação ordenada de primeira ordemEditar

  • 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. 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. 265–276. ISSN 0302-9743.
  • Idestam-Almquist, Peter (Jun 1993). "Generalization under Implication by Recursive Anti-Unification". Proc. 10th Conf. on Machine Learning. Morgan Kaufmann. pp. 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: ver acima

Antiunificação nominalEditar

  • Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (Jun 2013). Nominal Anti-Unification. Proc. RTA 2015. Vol. 36 of LIPIcs. Schloss Dagstuhl, 57-73. Software.

AplicaçõesEditar

  • 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ísticasEditar

  • Á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.[4]
  • Florestas sintáticas para parágrafos como grafos podem ser sujeitas a menor generalização geral.[5]
  • 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.[6][7]

Antiunificação de ordem superiorEditar

NotasEditar

Referências

  1. Complete generalization sets always exist, but it may be the case that every complete generalization set is non-minimal.
  2. Comon referred in 1986 to inequation-solving as "anti-unification", which nowadays has become quite unusual.
  3. E.g.  
  4. From a theoretical viewpoint, such a mapping exists, since both   and   are countably infinite sets; for practical purposes,   can be built up as needed, remembering assigned mappings   in a hash table.

Referências

  1. a b Plotkin, Gordon D. (1970). Meltzer, B.; Michie, D., eds. «A Note on Inductive Generalization». Edinburgh University Press. Machine Intelligence. 5: 153–163 
  2. a b Plotkin, Gordon D. (1971). Meltzer, B.; Michie, D., eds. «A Further Note on Inductive Generalization». Edinburgh University Press. Machine Intelligence. 6: 101–124 
  3. C.C. Chang; H. Jerome Keisler (1977). A. Heyting; H.J. Keisler; A. Mostowski; A. Robinson; P. Suppes, eds. Model Theory. Col: Studies in Logic and the Foundation of Mathematics. 73. [S.l.]: North Holland 
  4. Boris Galitsky; Josep Lluís de la Rose; Gabor Dobrocsi (2011). "Mapping Syntactic to Semantic Generalizations of Linguistic Parse Trees". FLAIRS Conference.
  5. Boris Galitsky; Kuznetsov SO; Usikov DA (2013). "Parse Thicket Representation for Multi-sentence Search". Lecture Notes in Computer Science7735: 1072–1091. doi:10.1007/978-3-642-35786-2_12
  6. Boris Galitsky; Gabor Dobrocsi; Josep Lluís de la Rosa; Sergei O. Kuznetsov (2010). "From Generalization of Syntactic Parse Trees to Conceptual Graphs"Lecture Notes in Computer Science6208: 185–190. doi:10.1007/978-3-642-14197-3_19
  7. 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:10.1016/j.datak.2012.07.003.