Unificação

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

Por exemplo, se x ∈ V é um símbolo de variável, 1 ∈ C é um símbolo de constante, e adicionar ∈ F₂ é 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 in-fixa 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 { x₁ ↦ t₁, ..., x_k ↦ t_k } se refere a substituição mapeada de cada variável x_i para o termo t_i, 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 {x₁ ↦ t₁, ..., x_k ↦ t_k}; isso significa (simultaneamente) substituir toda ocorrência de cada variável x_i de termo t por t_i. 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(x₁,a,g(z₁),y₁) é uma variante de f(x₂,a,g(z₂),y₂), desde que

f(x₁,a,g(z₁),y₁) { x₁ ↦ x₂, y₁ ↦ y₂, z₁ ↦ z₂ } = f(x₂,a,g(z₂),y₂) e f(x₂,a,g(z₂),y₂) { x₂ ↦ x₁, y₂ ↦ y₁, z₂ ↦ z₁ } = f(x₁,a,g(z₁),y₁). Por outro lado, f(x₁,a,g(z₁),y₁) não é uma variante de f(x₂,a,g(x₂),x₂), 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 { l₁ ≐ r₁, ..., l_n ≐ r_n } de equações potenciais, onde l_i, r_i ∈ T. Uma substituição σ é uma solução desse problema se l_iσ ≡ r_iσ 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

Diagrama triangular esquemático da unificação sintética dos termos t₁ e t₂ 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 F_n de símbolos de função n-ária) e em ≡ sendo igualdade sintática. Nessa forma, todo problema de unificação solúvel {l₁ ≐ r₁, ..., l_n ≐ r_n} 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 é, l₁σ = r₁σ ∧ ... ∧ l_nσ = r_nσ. Qualquer unificador do problema é coberto^{[nota 3]} pelo unificador mais geral de σ. O unificador mais geral é único em variantes: se S₁ e S₂ são ambos conjuntos soluções completos e mínimos do mesmo problema sintático de unificação, então S₁ = { σ₁ } e S₂ = { σ₂ } para algumas substituições σ₁ e σ₂, e xσ₁ é uma variante de xσ₂ 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(x₁), y ↦ f(f(x₁)), z ↦ f(x₁) }, { x ↦ f(f(x₁)), y ↦ f(f(f(x₁))), z ↦ f(f(x₁)) }, 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

Algoritmo da unificação de Robinson, 1965
Símbolos são ordenados tal que as variáveis precedem símbolos de função.
Termos são ordenados conforme o aumento do comprimento do termo escrito; igualmente, termos grandes
são ordenados lexicograficamente.[6] Para um conjunto T de termos, seu caminho
divergente p é o último caminho lexicograficamente onde dois termos membros
de T diferem. Seu conjunto divergente é o conjunto dos sub termos começando por p.
Formalmente: { t\|_p : t∈T }.[7]
Algoritmo:[8]
Dado um conjunto T de termos para ser unificado
Deixe σ inicialmente ser a identidade de substituição
Faça sempre:
se	Tσ é o conjunto unitário
então	retorne σ
fi
deixe D ser o conjunto divergente de Tσ
deixe s, t serem os dois últimos termos lexicograficamente em D
se	s não é uma variável ou s acontece em t
se não	retorne "NaoUnificaveis"
fi
σ := σ { s↦t }
Feito

Esse primeiro algoritmo dado por Robinson (1965) era bastante ineficiente; (ver o quadro). O algoritmo mais rápido originado em seguida foi o de Martelli, Montanari (1982). Esse papel também lista tentativas anteriores para achar um algoritmo de unificação eficiente, e declara que algoritmos de tempo linear foram descobertos independentemente por Martelli, Montanari (1976) e Paterson, Wegman (1978).

Dado um conjunto finito G = { s₁ ≐ t₁, ..., s_n ≐ t_n } de equações potenciais, o algoritmo aplica as regras para transformar isso em um conjunto equivalente de sentenças da forma { x₁ ≐ u₁, ..., x_m ≐ u_m } onde x₁, ..., x_m são variáveis distintas e u₁, ..., u_m são termos contendo nenhum dos x_i. Um conjunto dessa forma pode ser lido como uma substituição. Se não existe solução, o algoritmo elimina com ⊥; outros autores usam "Ω", "{}", or "fail" nesse caso. A operação de substituição de todas as ocorrências da variável x no problema G com termo t é denotado G {x ↦ t}. Para simplicidade, símbolos de constante são considerados como símbolos de funções contendo nenhum argumento.

G ∪ { t ≐ t }	⇒	G	apaga
G ∪ { f(s₀,...,s_k) ≐ f(t₀,...,t_k) }	⇒	G ∪ { s₀ ≐ t₀, ..., s_k ≐ t_k }	decompõe
G ∪ { f(s₀,...,s_k) ≐ g(t₀,...,t_m) }	⇒	⊥	if f ≠ g ou k ≠ m	conflito
G ∪ { f(s₀,...,s_k) ≐ x }	⇒	G ∪ { x ≐ f(s₀,...,s_k) }	troca
G ∪ { x ≐ t }	⇒	G{x↦t} ∪ { x ≐ t }	if x ∉ vars(t) e x ∈ vars(G)	elimina
G ∪ { x ≐ f(s₀,...,s_k) }	⇒	⊥	if x ∈ vars(f(s₀,...,s_k))	checa

Verificação de ocorrência

Uma tentativa de unificar a variável x com um termo contento x como um subtermo x≐f(...,x,...) iria conduzir a um termo infinito como solução para x, já que x iria ocorrer como um subtermo de si mesmo. No conjunto de (finito) termos de primeira ordem como definido acima, a equação x≐f(...,x,...) não possui solução; consequentemente a regra da eliminação talvez seja apenas aplicável se x ∉ vars(t). Desde que uma checagem adicional, chamada de seleção de ocorrência, diminui a velocidade do algoritmo, ele está omitido em maior parte dos sistemas Prolog. De um ponto de vista teórico, omitindo a checagem de quantidades para resolver equações sobre árvores infinitas, veja abaixo.

Prova da terminação

Para a prova de terminação do algoritmo, considere uma tripla <n_var,n_lhs,n_eqn> onde n_var é o número de variáveis que ocorrem mais de uma vez no conjunto de equações, n_lhs é o número de símbolo de função e constante à esquerda das equações potenciais, e n_eqn é o número de equações. Quando a regra de eliminação é aplicada, n_var decresce, desde que x é eliminado de G e mantendo somente em { x ≐ t }. Aplicando qualquer outra regra não pode aumentar n_var de novo. Quando a regra de decompsição, conflito, ou troca é aplicada, n_lhs decresce, desde que pelo menos à esquerda o f mais externo desaparece. Aplicando qualquer regra restante, deletar ou checar não pode aumentar n_lhs, mais decresce n_eqn. Finalmente, qualquer aplicação de regra decresce a tripla <n_var,n_lhs,n_eqn> com respeito a ordem lexicográfica, a qual é apenas possível com um número finito de termos.

Conor McBride observa que “expressando a estrutura a qual a unificação explora” em uma linguagem de tipo dependente como Epigram, Algoritmo de Robinson pode ser feito através da recursão do número de variáveis, em um caso em que uma prova de terminação separada torna-se desnecessária.

Exemplos de unificação sintática de termos de primeira ordem

Na convenção sintática da linguagem Prolog, um símbolo começado com uma letra maiúscula é um nome de variável; um símbolo começado com uma letra minúscula é um símbolo de unificação; a vírgula é usada como o operador lógico 'e'. Para notação matemática, x,y,z são usadas como variáveis, f,g como símbolos de funções, e a,b como constantes.

Notação Prolog	Notação Matemática	Substituição unificadora	Explicação
a = a	{ a = a }	{}	Sucesso. (tautologia)
a = b	{ a = b }	⊥	a e b não combinam
X = X	{ x = x }	{}	Sucesso. (tautologia)
a = X	{ a = x }	{ x ↦ a }	x é unificado com a constante a
X = Y	{ x = y }	{ x ↦ y }	x e y são semelhantes
f(a,X) = f(a,b)	{ f(a,x) = f(a,b) }	{ x ↦ b }	símbolos de função e constante combinam, x é unificado com a constante b
f(a) = g(a)	{ f(a) = g(a) }	⊥	f e g não combinam
f(X) = f(Y)	{ f(x) = f(y) }	{ x ↦ y }	x e y são semelhantes
f(X) = g(Y)	{ f(x) = g(y) }	⊥	f e g não combinam
f(X) = f(Y,Z)	{ f(x) = f(y,z) }	⊥	Falha. Os símbolos de função f tem aridades diferentes
f(g(X)) = f(Y)	{ f(g(x)) = f(y) }	{ y ↦ g(x) }	Unifica y com o termo g(x)
f(g(X),X) = f(Y,a)	{ f(g(x),x) = f(y,a) }	{ x ↦ a, y ↦ g(a) }	Unifica x coma constante a, e y como termo g(a)
X = f(X)	{ x = f(x) }	deveria ser ⊥	Retorna ⊥ em lógica de primeira ordem e em muitos dialetos modernos de Prolog (imposta pelo seleção de ocorrência). Correto no Prolog tradicionale em Prolog II, unificando x com um termo em loop x=f(f(f(f(...)))).
X = Y, Y = a	{ x = y, y = a }	{ x ↦ a, y ↦ a }	Ambos x e y são unificados pela constante a
a = Y, X = Y	{ a = y, x = y }	{ x ↦ a, y ↦ a }	Como acima (a ordem do conjunto de equações não importa)
X = a, b = X	{ x = a, b = x }	⊥	Falha. a e b não combinam (constantes), então x não pode ser unificado em ambos

Dois termos com uma grande árvore exponencial para sua última instância em comum. Sua representação em grafo (à direita, parte laranja) ainda é de tamanho linear.

O unificador mais geral de um problema de unificação sintática de primeira ordem de tamanho n talvez tenha um tamanho 2ⁿ. Por exemplo, o problema { (((a*z)*y)*x)*w ≐ w*(x*(y*(z*a))) } tem o unificador mais geral { z ↦ a, y ↦ a*a, x ↦ (a*a)*(a*a), w ↦ ((a*a)*(a*a))*((a*a)*(a*a)) }, (veja a figura). Em ordem para escapar do tempo de complexidade exponencial causado pelo blow-up, algoritmos avançados de unificação trabalham em grafos acíclicos dirigidos em vez de árvores.

Aplicação: unificação em programação em lógica

O conceito de unificação é uma das principais ideias por trás da programação em lógica, mais conhecida por pela linguagem Prolog. Isso representa o mecanismo de conteúdos obrigatórios de variáveis e pode ser visto como um tipo de atribuição de uma vez só. Em Prolog, essa operação é denotada pelo símbolo de igualdade =, mas é também reconhecido quando instanciámos variáveis (veja abaixo). Isso também é usado em outras linguagens através do uso do símbolo de igualdade =, mas também em conjunção com muitas operações, incluindo +, -, *, /. Algoritmos de tipo de inferência são tipicamente baseados em unificação.

Em Prolog:

Uma variável que não está instanciada —isto é, sem unificação anterior feita nela— pode ser unificada com um átomo, um termo, ou outra variável não instanciada, assim torna-se efetivamente sua semelhante. Em vários dialetos modernos de Prolog e em lógica de primeira ordem, uma variável não pode ser unificada com um termo que contém ela; isso é chamado de seleção de ocorrência.
Dois átomos pode somente ser unificados se eles são idênticos.
Similarmente, um termo pode ser unificado com outro termo se o símbolo da função do topo, a aridade dos termos são idênticas e se os parâmetros podem ser unificados simultaneamente. Note que isso é um comportamento recursivo.

Aplicação: inferência de tipo

Unificação é usada durante o tipo de inferência, por exemplo na linguagem funcional de programação Haskell. Um um sentido, o programador não precisa fornecer um tipo de informação para toda função, no outro sentido, isso é usado para detectar erros de escrita. A expressão de Haskell 1:['a','b','c'] não é corretamente escrita porque a construção da lista de função ":" é do tipo a->[a]->[a] e para o primeiro argumento "1" a variável tipo polimórfico "a" tem que denotar o tipo Int (inteiro) enquanto que "['a','b','c']" é do tipo [Char], mas "a" não pode ser Char e Int ao mesmo tempo.

Como em Prolog, um algoritmo para o tipo de inferência pode ser dado por:

Qualquer tipo de variável unifica com qualquer tipo de expressão, e é instanciado para essa expressão. Uma teoria específica talvez restrinja essa regra com a seleção de ocorrência.
Dois tipos de constante unificam somente se elas são do mesmo tipo.
Dois tipos de construções unificam somente se elas são aplicações do mesmo tipo de construtor e todos os seus tipos de componentes unificam recursivamente.

Devido a natureza declarativa, a ordem em uma sentença de unificações é (geralmente) sem importância.

Note que na terminologia da lógica de primeira ordem, um átomo é uma preposição básica e unificada similarmente para um termo de Prolog..

Unificação com sortes

Lógica polisortida permite uma atribuição de um tipo para cada termo, e para declarar um tipo s₁ um subtipo de um outro tipo s₂, comumente escrito como s₁ ⊆ s₂. Por exemplo, quando se questionando sobre criaturas biológicas, é útil declarar um tipo cachorro para ser um subtipo de um tipo animal. Sempre que um termo de algum tipo s é necessário, um termo de qualquer subtipo de s talvez possa ser fornecido no lugar. Por exemplo, assumindo a declaração da função mãe: animal → animal, e uma declaração constante feminino: cachorro, o termo mãe(feminino) é perfeitamente válido e possui o tipo animal. A fim de fornecer a informação que a mãe de um cachorro é um cachorro de volta, outra declaração mãe: cachorro → cachorro pode ser emitida; isso é chamado de overloading de função, similar a overloading em linguagem de programação.

Walther deu um algoritmo de unificação para termos em lógica de ordem aleatória, requerindo para qualquer dois tipos declarados s₁, s₂ sua interseção s₁ ∩ s₂ para ser declarada, também: se x₁ e x₂ é uma variável de tipo s₁ and s₂, respectivamente, a equação x₁ ≐ x₂ tem a solução { x₁ = x, x₂ = x }, onde x: s₁ ∩ s₂. Depois de incorporar esse algoritmo em um teorema de prova automático baseado em cláusulas, ele pode resolver um problema de benchmark traduzindo para lógica de ordem aleatória, assim reduzindo sua magnitude, como vários predicados unários são transformados em sortidos.

Smolka generalizou a lógica aleatória para permitir polimorfismo paramétrico. Em seu quadro, declarações de subtipo são propagadas para expressões de tipos complexos. Como um exemplo de programação, um tipo paramétrico de lista(X) pode ser declarado (com X sendo um tipo de parâmetro como em C++ template), e para uma declaração de subtipo int ⊆ float a relação list(int) ⊆ list(float) é automaticamente inferida, significando que cada lista de inteiros é também uma lista de floats.

Schmidt-Schauß generalizou a lógica de ordem aleatória para permitir declaração de termos. Como um exemplo, assumindo declarações de subtipos par ⊆ int e ímpar ⊆ int, uma declaração do termo como ∀i:int. (i+i):par permite declarar uma propriedade do inteiro em adição que não poderia ser expressada por overloading ordinário.

Unificação de termos infinitos

Prévias em árvores infinitas (em inglês):

B. Courcelle (1983). "Fundamental Properties of Infinite Trees" (PDF). Theoret. Comput. Sci. 25: 95–169. doi:10.1016/0304-3975(83)90059-2.
Michael J. Maher (Jul 1988). "Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees". Proc. IEEE 3rd Annual Symp. on Logic in Computer Science, Edinburgh. pp. 348–357.
Joxan Jaffar, Peter J. Stuckey (1986). "Semantics of Infinite Tree Logic Programming". Theoretical Computer Science 46: 141–158. doi:10.1016/0304-3975(86)90027-7.

Algoritmo da unificação, Prolog II (em inglês):

A. Colmerauer (1982). K.L. Clark and S.-A. Tarnlund, ed. Prolog and Infinite Trees. Academic Press.
Alain Colmerauer (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT. Proc. Int. Conf. on Fifth Generation Computer Systems. pp. 85–99.

Aplicações (em inglês):

Francis Giannesini, Jacques Cohen (1984). "Parser Generation and Grammar Manipulation using Prolog's Infinite Trees". J. Logic Programming 3: 253–265.

E-Unificação

E-Unificação é o problema de achar soluções para um dado conjunto de equações, levando em conta um alguns conhecimentos prévios equacionais E. O último é dado como um conjunto de igualdades universal. Para algum conjunto particular E, algoritmos de solução de equações (também conhecido como algoritmo da unificação E) tem sido idealizado; para outros isso tem sido provado que nenhum algoritmo pode existir.

Por exemplo, se a e b são constantes distintas, a equação x*a ≐ y*b não tem solução com respeito a pura unificação sintática, onde nada é conhecido sobre o operador *. Contudo, se o * é conhecido como comutativo, então a substituição { x ↦ b, y ↦ a } resolve a equação acima, desde que

x*a	{x ↦ b, y ↦ a}
=	b*a	pela aplicação da substituição
=	a*b	pela comutatividade de *
=	y*b	{x ↦ b, y ↦ a}	pela (conversão) aplicação da substituição

O conhecimento prévio E pode condizer com a comutatividade de * pela igualdade universal "u*v = v*u para todo u, v".

Conjunto de conhecimentos básicos E

Convenções de nome usadas
∀ u,v,w:	u(vw)	=	(uv)w	A	Associatividade de *
∀ u,v:	u*v	=	v*u	C	Comutatividade de *
∀ u,v,w:	u*(v+w)	=	uv+uw	D_l	Distribuição à esquerda de * sobre +
∀ u,v,w:	(v+w)*u	=	vu+wu	D_r	Distribuição À direita de * sobre +
∀ u:	u*u	=	u	I	Idempotencia de *
∀ u:	n*u	=	u	N_l	Elemento neutro à esquerda n com respeito a *
∀ u:	u*n	=	u	N_r	Elemento neutro à direita n com respeito a *

É dito que unificação é decidível para uma teoria, se um algoritmo de unificação tem sido idealizado para que termine com qualquer problema de entrada. É dito que a unificação é semi-decidível para uma teoria, se um algoritmo de unificação tem sido idealizado para que termine com qualquer problema de entrada resolvível, mas talvez continue procurando para sempre por soluções de um problema de entrada sem solução.

Unificação é decidível para as seguintes teorias:

A
A,C
A,C,I
A,C,N_l^{[nota 4]}
A,I
A,N_l,N_r (monoid)
C
Anel booleano
Grupo abeliano, mesmo se a assinatura é expandida pela arbitrariedade adicional dos símbolos (mas não pelos axiomas)
K4 álgebras modais

Unificação é semi-decidível para as seguintes teorias:

A,D_l,D_r
A,C,D_l^{[nota 4]}
Anel comutativo

Paramodulação unilateral

Se tem um sistema de redução de termos R disponível para E, o algoritmo de paramodulação unilateral pode ser usado para enumerar todas as soluções das equações dadas.

Regras unilaterais de paramodulação
G ∪ { f(s₁,...,s_n) ≐ f(t₁,...,t_n) }	; S	⇒	G ∪ { s₁ ≐ t₁, ..., s_n ≐ t_n }	; S	decompõe
G ∪ { x ≐ t }	; S	⇒	G { x ↦ t }	; S{x↦t} ∪ {x↦t}	se a variável x não ocorrer em t	elimina
G ∪ { f(s₁,...,s_n) ≐ t }	; S	⇒	G ∪ { s₁ ≐ u₁, ..., s_n ≐ u_n, r ≐ t }	; S	se f(u₁,...,u_n) → r é uma regra de R	modifica
G ∪ { f(s₁,...,s_n) ≐ y }	; S	⇒	G ∪ { s₁ ≐ y₁, ..., s_n ≐ y_n, y ≐ f(y₁,...,y_n) }	; S	se y₁,...,y_n são novas variáveis	imita

Começando com G sendo o problema de unificação para ser resolvido e S sendo a substituição identidade, regras são aplicadas não-deterministicamente até que o conjunto vazio apareça como o atual G, no qual caso o S atual é uma substituição unificável. Dependendo na ordem em que são aplicadas as regras de paramodulação, na escolha da atual equação de G, e na escolha de regras de R em modifcar, caminhos computacionais diferentes são possíveis. Apenas alguns caminhos conduzem para uma solução, enquanto outros terminam em um G ≠ {} onde nenhuma regra adiante é aplicável (isto é,. G = { f(...) ≐ g(...) }).

Exemplo de termo de redução do sistema R
1	app(nil,z)	→ z
2	app(x.y,z)	→ x.app(y,z)

Por exemplo, um sistema de termo reduzido R é usado definindo o operador anexo de listas construidos de cons e nil; onde cons(x,y) é escrito na notação infixa como x.y para brevidade; isto é. app(a.b.nil,c.d.nil) → a.app(b.nil,c.d.nil) → a.b.app(nil,c.d.nil) → a.b.c.d.nil demonstra a concatenação das listas a.b.nil e c.d.nil, empregando a regra de redução rule 2,2, e 1. A teoria equacional E correspondente a R é o fechamento de R, ambos vistos como relações binária em termos. Por exemplo, app(a.b.nil,c.d.nil) ≡ a.b.c.d.nil ≡ app(a.b.c.d.nil,nil). O algoritmo paramodular enumera as soluções para equações com respeito a E quando alimentado com o exemplo R.

Um exemplo de caminho de computação bem sucedido para o problema de unificação { app(x,app(y,x)) ≐ a.a.nil } é mostrado abaixo. Para evitar confronto com nome de variáveis, regras de redução são constantemente renomeadas a cada tempo antes de seu uso pela regra da modificação; v₂, v₃, ... são nomes de variáveis gerados computacionalmente para esse propósito. Em cada linha, a equação escolhida de G é destacada em vermelho. A cada tempo que a regra da modificação é aplicada, a regra de redução escolhida (1 or 2) é indicada em parênteses. A partir da última linha, o substituição unificadora S = { y ↦ nil, x ↦ a.nil } pode ser obtida. De fato, app(x,app(y,x)) {y↦nil, x↦ a.nil } = app(a.nil,app(nil,a.nil)) ≡ app(a.nil,a.nil) ≡ a.app(nil,a.nil) ≡ a.a.nil resolve o problema dado. Um segundo caminho computacional bem sucedido é obtido pela escolha de "modifica(1), modifica(2), modifica(2), modifica(1)" conduzindo para a substituição S = { y ↦ a.a.nil, x ↦ nil }; que não é mostrada aqui. Nenhum outro caminho conduz ao sucesso.

Exemplo de unificação computacional
Regra usada	G	S
{ app(x,app(y,x)) ≐ a.a.nil }	{}
modifica(2)	⇒	{ x ≐ v₂.v₃, app(y,x) ≐ v₄, v₂.app(v₃,v₄) ≐ a.a.nil }	{}
decompõe	⇒	{ x ≐ v₂.v₃, app(y,x) ≐ v₄, v₂ ≐ a, app(v₃,v₄) ≐ a.nil }	{}
elimina	⇒	{ app(y,v₂.v₃) ≐ v₄, v₂ ≐ a, app(v₃,v₄) ≐ a.nil }	{ x ↦ v₂.v₃ }
elimina	⇒	{ app(y,a.v₃) ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ x ↦ a.v₃ }
modifica(1)	⇒	{ y ≐ nil, a.v₃ ≐ v₅, v₅ ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ x ↦ a.v₃ }
elimina	⇒	{ y ≐ nil, a.v₃ ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ x ↦ a.v₃ }
elimina	⇒	{ a.v₃ ≐ v₄, app(v₃,v₄) ≐ a.nil }	{ y ↦ nil, x ↦ a.v₃ }
modifica(1)	⇒	{ a.v₃ ≐ v₄, v₃ ≐ nil, v₄ ≐ v₆, v₆ ≐ a.nil }	{ y ↦ nil, x ↦ a.v₃ }
elimina	⇒	{ a.v₃ ≐ v₄, v₃ ≐ nil, v₄ ≐ a.nil }	{ y ↦ nil, x ↦ a.v₃ }
elimina	⇒	{ a.nil ≐ v₄, v₄ ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
elimina	⇒	{ a.nil ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
decompõe	⇒	{ a ≐ a, nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
decompõe	⇒	{ nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
decompõe	⇒	{}	{ y ↦ nil, x ↦ a.nil }

Estreitamento

Diagrama do triângulo da etapa estreitamento de s ~› t na posição p no termo s, com substituição unificadora σ (última linha), usando a regra de redução l → r (primeira linha)

Se R é um sistema de redução de termos convergente para E, uma aproximação alternativa para a seção anterior consiste em aplicações sucessivas da "etapa de estreitamento"; isso irá numerar eventualmente todas as soluções da equação dada. A etapa de estreitamento (veja a figura) consiste em:

escolher um subtermo não variável do termo atual,
sintaticamente unificando se com à esquerda de uma regra de R, e
substituindo a regra à direita instanciada dentro do termo instanciado.

Formalmente, se l → r é uma cópia renomeada de uma regra de redução de R, tendo nenhuma variável em comum com um temro de s, e o subtermo s|_p não é uma variável e é unificável com l pelo unificador mais geral σ, então s pode ser estreito para o termo t = sσ[rσ]_p, isto é, para o termo sσ, com o subtermo pré-alocado por rσ. A situação que s pode ser estreito para t é comummente denotado como s ~› t. Intuitivamente, uma sequência de passos de estreitamento t₁ ~› t₂~› ... ~› t_n pode ser pensada como a sequência dos passos da redução t₁ → t₂ → ... → t_n, mas com o termo inicial t₁ sendo mais adiante e adiante instanciado, como necessário para fazer cada umas das regras aplicáveis.

O exemplo acima de paramodulação computacional corresponde à seguinte sequência de estreitamento ("↓" indicando instanciação no local):

app(x, app y, x))

↓ ↓ x ↦ v₂.v₃

app(v₂.v_3, app(y, v₂.v₃)) → v₂.app(v₃,app(y, v₂.v₃))

↓ y ↦ nil

v₂.app(v₃,app(nil, v₂.v₃)) → v₂.app(v₃, v₂.v₃)

↓ v₃ ↦ nil

v₂.app(nil, v₂.nil) → v₂.v₂.nil'

O último termo, v₂.v₂.nil pode ser sintaticamente unificado com o original à direita do termo a.a.nil.

O lema de estreitamento garante que sempre que uma instância de um termo s pode ser reduzida para um termo t pela convergência do sistema de redução de termos, então s e t podem ser estreitados e reduzidos para um termo s’ e t’, respectivamente, tal que t’ é uma instância de s’. Formalmente: sempre que sσ →^* t mantém para alguma substituição σ, então existe termos s’, t’ tal que s ~›^* s’ e t →^* t’ e s’τ = t’ para alguma substituição τ.

Unificação de alta ordem

Várias aplicações requerem outra para considerar a unificação de um tipo de termo de lambda em vez de termos de primeira ordem. Tal unificação é casualmente chamada de unificação de alta ordem. Um ramo bem estudado de unificação de alta ordem é o problema de unificar um tipo simples de módulo de termos de lambda a igualdade determinada por conversões αβη. Tais problemas de unificação não tem a maioria dos unificadores gerais. Enquanto unificação de alta ordem é indecidível, Gérard Huet deu um algoritmo de (pré-)unificação semi-decidível que permite uma pesquisa sistemática de espaços de unificadores (generalizando o algoritmo de unificação de Martelli-Montanari com regras para termos contendo variáveis de alta ordem) que parece funcionar bem na prática. Huet e Gilles Dowek escreveram artigos mensurando esse tópico.

Dale Miller descreveu o que é agora chamado de padrão de unificação de alta ordem. Esse subconjunto de unificação de alta ordem é decide e resolve problemas de unificação que possuem os unificadores mais gerais. Muitos sistemas computacionais que contém unificação de alta ordem, assim como as linguagens de programação da lógica de alta ordem λProlog e Twelf, frequentemente implementam apenas um fragmento do padrão e não uma completa unificação de alta ordem.

Em linguagens computacionais, uma das teorias mais influentes de elipses é que elipses são representadas por variáveis livres as quais os valores são determinados usando a unificação de alta ordem. Por exemplo, a representação semântica de "Jon likes Mary e Peter fazem também" é como(j; m)R(p) e o valor de R (a representação semântica da elipse) é determinada pela equação como (j; m) = R(j). O processo de resolução desse tipo de equação é chamado de unificação de alta ordem.

uPor exemplo, o problema de unificação { f(a, b, a) ≐ d(b, a, c) }, onde a única variável é f, tem as soluções {f ↦ λx.λy.λz.d(y, x, c) }, {f ↦ λx.λy.λz.d(y, z, c) }, {f ↦ λx.λy.λz.d(y, a, c) }, {f ↦ λx.λy.λz.d(b, x, c) }, {f ↦ λx.λy.λz.d(b, z, c) } e {f ↦ λx.λy.λz.d(b, a, c) }.

Wayne Snyder deu uma generalização da unificação de alta ordem e unificação E, isto é, um algoritmo para unificar os módulos de termos lambda uma equação teórica.

Ver também

Notas

↑ nesse caso, ainda existe um conjunto de substituição completo (isto é, o conjunto de todas as soluções); contudo, cada conjunto contém membros redundantes.
↑ isto é, a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a.
↑ formalmente: cada unificador τ satisfaz ∀x: xτ = (xσ)ρ para alguma substituição ρ.
↑ na presença do igualdade C, igualdades N_l e N_r são equivalentes, similar para D_l e D_r_.

Referências

Franz Baader and Tobias Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
Franz Baader and Wayne Snyder, Unification Theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001.
Joseph Goguen, What is Unification?.
Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite Systems, in: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science, vol.B Formal Models and Semantics, Elsevier, 1990, pp. 243–320
Kevin Knight (Mar 1989). "Unification: A Multidisciplinary Survey" (PDF). ACM Computing Surveys 21 (1): 93–124. doi:10.1145/62029.62030.
Alex Sakharov, "Unification", MathWorld.