Unificação, em ciência da computação e na lógica, é um processo algorítmico de solução de equações entre expressões simbólicas.
Dependendo de quais expressões (também chamadas de termos) são permitidas ocorrer em um conjunto de equações (também chamado de problema da unificação), e quais expressões são consideradas iguais, diversas estruturas de unificação são distinguidas. Se variáveis de alta ordem, isto é, variáveis que representam funções, são permitidas em uma expressão, o processo é chamado de unificação de alta ordem, ou, caso contrário, é chamado de unificação de primeira ordem. Se exige-se uma solução que faça com que ambos os lados de cada equação sejam literalmente iguais, o processo é chamado de unificação sintática, ou, caso contrário, unificação semântica, ou unificação equacional, ou unificação E, ou unificação módulo uma teoria.
A solução de um problema de unificação é denotada como uma substituição, isto é, um mapeamento atribuindo um valor simbólico a cada variável das expressões do problema. Um algoritmo de unificação deve computar, para um dado problema, um conjunto de substituição completo e mínimo, isto é, um conjunto cobrindo todas as soluções e com nenhum membro redundante. Dependendo da estrutura, um conjunto de substituição completo e mínimo talvez contenha nenhum, ou uma quantidade finita, ou infinita de membros. [nota1] Em algumas estruturas é geralmente impossível decidir se existe alguma solução. Para a unificação sintática de primeira ordem, Martelli e Montanari desenvolveram um algoritmo capaz de informar a inexistência de uma solução ou computar um único conjunto de substituição completo e mínimo contendo o chamado unificador mais geral.
Por exemplo, usando x, y, z como variáveis e o único conjunto de equação { cons(x,cons(x,nil)) = cons(2,y) } é um problema unificação sintática de primeira ordem que tem a substituição { x ↦ 2, y ↦ cons(2,nil) } como uma única solução. O problema da unificação sintática de primeira ordem { y = cons(2,y) } não possui uma solução sobre o conjunto de termos finitos; contudo, possui como solução única { y ↦ cons(2,cons(2,cons(2,...))) } sobre o conjunto de árvores infinitas. O problema da unificação semântica de primeira ordem { a⋅x = x⋅a } possui toda substituição da forma { x ↦ a⋅...⋅a } como uma solução em um semi grupo, isto é, se (⋅) é considerado associativo; o mesmo problema, visto em um grupo abeliano, onde (⋅) é considerado também como comutativo, tem qualquer substituição como uma solução. O único conjunto { a = y(x) } é um problema se unificação sintático de segunda ordem, desde que y seja uma função variável. Uma solução é { x ↦ a, y ↦ (função identidade) }; outra solução é { y ↦ (função constante mapeando cada valor para a), x ↦ (qualquer valor) }.
A primeira investigação formal de unificação pode ser atribuída a John Alan Robinson, quem usou a unificação sintática de primeira ordem como um bloco básico de construção em seu processo de resolução para a lógica de primeira ordem, um bom avanço na tecnologia de raciocínio automatizado, uma vez que isso eliminou uma fonte de explosão combinatória: busca por instanciação de termos. Hoje, o raciocínio automatizado continua sendo a principal área de aplicação da unificação. A unificação sintática de primeira ordem é usada na lógica de programação e na implementação de sistema de tipos na linguagem de programação, especialmente nos tipos de algoritmos de inferência baseados em Hindley–Milner. A unificação semântica é usada em solucionadores SMT e em algoritmos de reescrita de termos. Unificação de alta ordem é usada em assistentes de provas, por exemplo, Isabelle e Twelf, e formas restritas da unificação de alta ordem (padrão de unificação de alta ordem) são usadas em algumas implementações de linguagens de programação, no caso de lambdaProlog. Como padrões de alta ordem são expressivos, seu processo de unificação associada ainda retêm propriedades teóricas próximas a unificação de primeira ordem.
Definições formais comuns Pré-requisitos Formalmente, uma abordagem de unificação pressupõe Um conjunto infinito V de variáveis. Para unificação de alta ordem, é conveniente escolher V disjunto do conjunto de variáveis ligadas ao Cálculo Lambda. Um conjunto T de termos tal que V ⊆ T. Para a unificação de primeira ordem, T é usualmente o conjunto de termos de primeira ordem (termos construídos a partir de variáveis e símbolos de funções) e termos de lambda (termos contendo algumas variáveis de alta ordem), respectivamente. Um mapeamento vars: T → ℙ(V), atribuindo para cada termo t do conjunto vars(t) ⊊ V de variáveis livres ocorrendo em t. Uma relação de equivalência ≡ em T, indicando quais termos são considerados iguais. Para unificação de alta ordem, usualmente t ≡ u se t e u são equivalentes em alpha. Para unificação E de primeira ordem, ≡ reflete no conhecimento prévio sobre certos símbolos de função; por exemplo, se ⊕ é considerado comutativo, t ≡ u se u resulta de t pela troca dos argumentos de ⊕ em algumas (possivelmente todas) ocorrências. [nota 2] Se não existe conhecimento prévio completo, então somente literalmente, ou sintaticamente, termos idênticos são considerados iguais; nesse caso, ≡ é chamado de teoria livre (porque é um objeto livre), de teoria vazia (porque o conjunto de sentenças equacionais, ou o conhecimento prévio, é vazio), de teoria de funções não interpretadas (porque a unificação é feita em termos não interpretados), ou de teoria de construtores (porque todos os símbolos de funções são construídos apenas de backup de termos, em vez de operar sobre eles).
Termo de primeira ordem Dado um conjunto V de símbolo de variáveis, um conjunto C de símbolos constantes e conjuntos Fn de símbolos de funções n-árias, também chamado de operador de símbolos, para cada número natural n ≥ 1, o conjunto de (primeira ordem não aleatórios) de termos T é recursivamente definido para ser o menor conjunto com as seguintes propriedades: todo símbolo de variável é um termo: V ⊆ T, todo símbolo de constante é um termo: C ⊆ T, de todos os n termos t1,...,tn, e todo símbolo de função n-ária f ∈ Fn, um termo maior f(t1,...,tn) pode ser construído. Por exemplo, se x ∈ V é um símbolo de variável, 1 ∈ C é um símbolo de constante, e adicionar ∈ F2 é um símbolo de função binária, então x ∈ T, 1 ∈ T, e (consequentemente) adicionar(x,1) ∈ T pelo primeiro, segundo, e terceiro tópicos construindo as regras, respectivamente. O último termo é usualmente escrito como x+1, usando a notação infixa e o mais comum o símbolo de operação + por conveniência.
Termo de alta ordem Substituição Uma substituição é um mapeamento σ: V → T de variáveis para termos; a notação { x1 ↦ t1, ..., xk ↦ tk } se refere a substituição mapeada de cada variável xi para o termo ti, para i=1,...,k, e todo outra variável para si mesma. Aplicando essa substituição para um termo t é escrito em notação pós-fixa como t {x1 ↦ t1, ..., xk ↦ tk}; isso significa (simultaneamente) substituir toda ocorrência de cada variável xi de termo t por ti. O resultado tσ da aplicação da substituição σ para um termo t é chamado de instância do termo t. Assim como um exemplo de primeira ordem, aplicando a substituição { x ↦ h(a,y), z ↦ b } ao termo: f( x, a, g( z ), y) resulta em f( h(a,y), a, g( b ), y).
Generalização, especialização Se um termo t tem uma instância equivalente a um termo u, isto é, se tσ ≡ u para alguma substituição σ, então t é chamado de mais geral do que u, e u é chamado de mais especial que t. Por exemplo, x ⊕ a é mais geral que a ⊕ b se ⊕ é comutativo, desde então, (x ⊕ a) {x↦b} = b ⊕ a ≡ a ⊕ b.
Se ≡ é a identidade (sintática) de termos, o termo pode ser mais geral e mais especial que outro somente se ambos os termos diferem em seus nomes de variáveis, e não em sua estrutura sintática; esses termos são chamados de variante, ou renomeação de um termo p'r'o outro. Por exemplo, f(x1,a,g(z1),y1) é uma variante de f(x2,a,g(z2),y2), desde que
f(x1,a,g(z1),y1) { x1 ↦ x2, y1 ↦ y2, z1 ↦ z2 } = f(x2,a,g(z2),y2) e f(x2,a,g(z2),y2) { x2 ↦ x1, y2 ↦ y1, z2 ↦ z1 } = f(x1,a,g(z1),y1). Por outro lado, f(x1,a,g(z1),y1) não é uma variante de f(x2,a,g(x2),x2), desde que nenhuma substituição pode transformar o último termo no anterior. O último termo é portanto mais especial que o anterior.
Para arbitrariedade ≡, um termo talvez seja mais geral e mais especial do que um termo estruturalmente diferente. Por exemplo, se ⊕ é idempotente, isto é, se sempre x ⊕ x ≡ x, então o termo x ⊕ y é mais geral que (x ⊕ y) {x ↦ z, y ↦ z} = z ⊕ z ≡ z, e vice-versa z é mais geral que z {z ↦ x ⊕ y} = x ⊕ y, embora x⊕y e z são de uma estrutura diferente.
Uma substituição σ é mais especial , ou coberta por uma substituição τ se xσ é mais especial que xτ para toda variável x. Por exemplo, { x ↦ f(u), y ↦ f(f(u)) } é mais especial que { x ↦ z, y ↦ f(z) }, desde que f(u) e f(f(u)) é mais especial que z e f(z), respectivamente.
Problema da unificação, conjunto solução Um problema de unificação é um conjunto finito { l1 ≐ r1, ..., ln ≐ rn } de equações potenciais, onde li, ri ∈ T. Uma substituição σ é uma solução desse problema se liσ ≡ riσ para i=1,...,n. Tal substituição é também chamada de unificadora de um problema de unificação. Por exemplo, se ⊕ é associativo, o problema de unificação { x ⊕ a ≐ a ⊕ x } tem as soluções {x ↦ a}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a}, etc., enquanto o problema { x ⊕ a ≐ a } não tem solução.
Para um dado problema de unificação, um conjunto S de unificadores é chamado de completo se toda solução de substituição é coberta por alguma substituição σ ∈ S; o conjunto S é chamado de mínimo se nenhum de seus membros cobre outro membro.
Unificação sintática de termos de primeira ordem thumb|Diagrama triangular esquemático da unificação sintética dos termos t1 e t2 pela substituição σ Unificação sintática de termos de primeira ordem é a forma de unificação mais usada. Ela é baseada em T sendo o conjunto de termos de primeira ordem (sobre algum dado conjunto V de variáveis, C de constantes e Fn de símbolos de função n-ária) e em ≡ sendo igualdade sintática. Nessa forma, todo problema de unificação solúvel {l1 ≐ r1, ..., ln ≐ rn} tem um único conjunto solução completo, e obviamente mínimo {σ}. Seu membro σ é chamado de unificador mais geral do problema. Os termos à direita e à esquerda de cada equação potencial se tornam sintaticamente iguais quando o unificador mais geral é aplicado, isto é, l1σ = r1σ ∧ ... ∧ lnσ = rnσ. Qualquer unificador do problema é coberto[nota 3] pelo unificador mais geral de σ. O unificador mais geral é único em variantes: se S1 e S2 são ambos conjuntos soluções completos e mínimos do mesmo problema sintático de unificação, então S1 = { σ1 } e S2 = { σ2 } para algumas substituições σ1 e σ2, e xσ1 é uma variante de xσ2 para cada variável x ocorrendo no problema.
Por exemplo, o problema da unificação { x ≐ z, y ≐ f(x) } tem um unificador { x ↦ z, y ↦ f(z) }, porque x { x ↦ z, y ↦ f(z) } = z = z { x ↦ z, y ↦ f(z) }, e y { x ↦ z, y ↦ f(z) } = f(z) = f(x) { x ↦ z, y ↦ f(z) } . Esse é também o unificador mais geral. Outros unificadores para o mesmo problema são { x ↦ f(x1), y ↦ f(f(x1)), z ↦ f(x1) }, { x ↦ f(f(x1)), y ↦ f(f(f(x1))), z ↦ f(f(x1)) }, e assim por diante; existem infinitos unificadores similares.
Como outro exemplo, o problema g(x,x) ≐ f(y) não possui solução com respeito a ≡ sendo a identidade de literais, já que qualquer substituição aplicada à direita e à esquerda vai manter o mais externo g e f, respectivamente, e termos com diferentes símbolos de função mais externos são sintaticamente diferentes.
Um algoritmo de unificação