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; 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 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. 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 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 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 $\equiv$ em $T$, indicando quais termos são considerados iguais. Para antiunificação de ordem superior, usualmente $t\equiv u$ se $t$ e $u$ são alpha equivalentes. Para primeira ordem E-antiunificação, $\equiv$ reflete o conhecimento base sobre certos símbolos de função; por examplo, se $\oplus$ é considerado comutativo, $t\equiv u$ se $u$ resulta de $t$ trocando os argumentos de $\oplus$ em algumas(possivelmente todas) ocorrências. 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 $V$ de símbolos variáveis, um conjunto $C$ de símbolos de constante e conjuntos $F_n$ de símbolos de funções $n$-árias, também chamado de operador de símbolos, para cada número natural $n\ge 1$ o conjunto de (não-ordenado de primeira ordem) termos $T$ é definido recursivamente para ser o menor conjunto com as seguintes propriedades:

• 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₁,...,t_n, e a cada símbolo de função n-ária f ∈ F_n, um termo maior pode ser construído.

Por exemplo, se x ∈ V é um símbolo de variável, 1 ∈ C é um símbolo de constante, e add ∈ F₂ é um símbolo de função binária e, então, x ∈ T, 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.

Substituição

Uma substituição é um mapeamento $\sigma :V⟶T$ de variáveis para termos; a notação$\{x_1\mapsto t_1,\dots ,x_k\mapsto t_k\}$ se refere a uma substituição mapeando cada variável $x_i$ para o termo $t_i$, para $i=1,\dots ,k$, e cada outra variável para ela mesma. Aplicando essa substitutição a um termo t é escrito em notação pós-fixa como $t\{x_1\mapsto t_1,\dots ,x_k\mapsto t_k\}$; isso significa (simultaneamente) realocar cada ocorrência de cada variável $x_i$ no termo t por $t_i$. 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 $\{x\mapsto h(a,y),z\mapsto b\}$ ao termo

Predefinição:Math	Predefinição:Math	Predefinição:Math	z	Predefinição:Math	resulta em
Predefinição:Math	Predefinição:Math	Predefinição:Math	b	Predefinição:Math	.

Generalização, especialização

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

Se $\equiv$ é 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, $f(x_1,a,g(z_1),y_1)$ é um variante $f(x_2,a,g(z_2),y_2)$, desde que $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)$ e$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)$. Contudo, $f(x_1,a,g(z_1),y_1)$ não é um variante de $f(x_2,a,g(x_2),x_2)$, já que nenhuma substituição pode transformar o último termo no primeiro, embora $\{x_1\mapsto x_2,z_1\mapsto x_2,y_1\mapsto x_2\}$ atinge a direção inversa. O último termo é, portanto, mais especial do que o anterior.

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

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

Um problema de antiunificação é um par $⟨t_1,t_2⟩$ de termos. Um termo $t$ é uma generalização comum, ou antiunificador, de $t_1$ e $t_2$ se $t{\sigma }_1\equiv t_1$ e $t{\sigma }_2\equiv t_2$ para alguma substituição ${\sigma }_1,{\sigma }_2$. Para um dado  problema de antiunificação, um conjunto $S$ de antiunificadores é chamado completo se cada generalização subsume algum termo $t\in S$; o conjunto $S$ é 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 $T$ sendo o conjunto de termos de primeira ordem (sobre dado algum conjunto $V$ de variáveis, $C$ de constantes e $F_n$ de símbolos de função $n$-ária) e em $\equiv$ sendo igualdade sintática. Nesta estrutura, cada problema de antiunificação $⟨t_1,t_2⟩$ tem uma completo, e obviamente mínimo, conjunto unitário solução $\{t\}$. Seu membro $t$ é chamado de menor generalização geral (mgg) do problema, ele tem uma instância sintaticamente igual a $t_1$ e uma outra sintaticamente igual a $t_2$. Qualquer generalização comum de $t_1$ e $t_2$ subsume $t$. O mgg é único para cada variante: se $S_1$ e $S_2$ são ambos conjuntos solução completos e mínimos do mesmo problema de antiunificação sintática, então $S_1=\{s_1\}$ e $S_2=\{s_2\}$ para algum termo $s_1$ e $s_2$, que sãorenomeados de cada outro.

Plotkin tem dado um algoritmo para computar o lgg de dois termos dados. Isso pressupõe um mapeamento injetivo $\varphi :T\times T⟶V$, isto é, um mapeamento atribuindo cada par $s,t$ de termos uma própria variável $\varphi (s,t)$, tal que dois pares não compartilham da mesma variável. O algoritmo consiste em duas regras: 

$f(s_1,\dots ,s_n)\bigsqcup f(t_1,\dots ,t_n)$	$⇝$	$f(s_1\bigsqcup t_1,\dots ,s_n\bigsqcup t_n)$
$s\bigsqcup t$	$⇝$	$\varphi (s,t)$	se a regra anterior não for aplicável

Por exemplo, $(0*0)\bigsqcup (4*4)⇝(0\bigsqcup 4)*(0\bigsqcup 4)⇝\varphi (0,4)*\varphi (0,4)⇝x*x$; 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 ordem

• Predefinição:Citation
• Predefinição:Citation
• 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 equacionais

• Uma operação associativa e comutativa: Predefinição:Citation; Predefinição:Citation
• 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. 86–91. 
• Monóides livres: Predefinição:Citation
• Classes regulares de congruência: Predefinição:Citation; Burghardt, Jochen (2005). "E-Generalization Using GrammarsPredefinição:Ligação inativa" (PDF). Artificial Intelligence Journal. Elsevier. 165 (1): 1–35. doi:10.1016/j.artint.2005.01.008. 
• A-, C-, AC-, ACU- Teorias com tipos ordenados: Alpuente, Maria; Escobar, Santiago; Espert, Javier; Meseguer, Jose (2014). "A modular order-sorted equational generalization algorithm" (PDF). Information and Computation. Elsevier. 235: 98–136. doi: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. 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 nominal

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

Antiunificação de ordem superior

• Cálculos de construções: Frank Pfenning (Jul 1991). "Unification and Anti-Unification in the Calculus of Constructions" (PDF). Proc. 6th LICS. Springer. pp. 74–85. 
• 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). A Variant of Higher-Order Anti-Unification. Proc. RTA 2013. Vol. 21 of LIPIcs. Schloss Dagstuhl, 113-127. Software.
• Substituições restritas de ordem superior: Predefinição:Citation; Predefinição:Citation