Unificação (ciência da computação) - Unification (computer science)

Na lógica e na ciência da computação , a unificação é um processo algorítmico de resolução de equações entre expressões simbólicas .

Dependendo de quais expressões (também chamadas de termos ) podem ocorrer em um conjunto de equações (também chamado de problema de unificação ), e quais expressões são consideradas iguais, várias estruturas de unificação são distinguidas. Se variáveis ​​de ordem superior, ou seja, variáveis ​​que representam funções , são permitidas em uma expressão, o processo é chamado de unificação de ordem superior , caso contrário, unificação de primeira ordem . Se uma solução é necessária para tornar ambos os lados de cada equação literalmente iguais, o processo é chamado de unificação sintática ou livre , caso contrário, unificação semântica ou equacional , ou unificação E , ou teoria do módulo de unificação .

A solução de um problema de unificação é denotada como substituição , ou seja, um mapeamento que atribui um valor simbólico a cada variável das expressões do problema. Um algoritmo de unificação deve calcular para um determinado problema um conjunto de substituição completo e mínimo , ou seja, um conjunto que cobre todas as suas soluções e não contém membros redundantes. Dependendo da estrutura, um conjunto de substituição completo e mínimo pode ter no máximo um, no máximo finitos muitos, ou possivelmente infinitos muitos membros, ou pode não existir de todo. Em algumas estruturas, geralmente é impossível decidir se existe alguma solução. Para a unificação sintática de primeira ordem, Martelli e Montanari forneceram um algoritmo que relata a insolubilidade ou calcula um conjunto de substituição de singleton completo e mínimo contendo o assim chamado unificador mais geral .

Por exemplo, usando x , y , z como variáveis, o conjunto de equações singleton { cons ( x , cons ( x , nil )) = cons (2, y )} é um problema de unificação sintática de primeira ordem que tem a substituição { x ↦ 2, y ↦ cons (2, nil )} como sua única solução. O problema de unificação sintática de primeira ordem { y = cons (2, y )} não tem solução sobre o conjunto de termos finitos ; entretanto, ele tem a única solução { y ↦ cons (2, cons (2, cons (2, ...)))} sobre o conjunto de árvores infinitas . O problema de unificação semântica de primeira ordem { a ⋅ x = x ⋅ a } tem cada substituição da forma { x ↦ a ⋅ ... ⋅ a } como uma solução em um semigrupo , ou seja, se (⋅) é considerado associativo ; o mesmo problema, visto em um grupo abeliano , onde (⋅) é considerado também comutativo , tem qualquer substituição como solução. O conjunto singleton { a = y ( x )} é um problema de unificação sintática de segunda ordem, uma vez que y é uma variável de função. Uma solução é { x ↦ a , y ↦ ( função de identidade )}; outro é { y ↦ ( função constante mapeando cada valor para a ), x ↦ (qualquer valor) }.

Um algoritmo de unificação foi descoberto por Jacques Herbrand , enquanto uma primeira investigação formal pode ser atribuída a John Alan Robinson , que usou a unificação sintática de primeira ordem como um bloco de construção básico de seu procedimento de resolução para lógica de primeira ordem, um grande passo em frente em tecnologia de raciocínio automatizado , pois eliminou uma fonte de explosão combinatória: a busca pela instanciação de termos. Hoje, o raciocínio automatizado ainda é a principal área de aplicação da unificação. A unificação sintática de primeira ordem é usada em programação lógica e implementação de sistema de tipo de linguagem de programação , especialmente em algoritmos de inferência de tipo baseados em Hindley-Milner . A unificação semântica é usada em resolvedores SMT , algoritmos de reescrita de termos e análise de protocolo criptográfico . A unificação de ordem superior é usada em assistentes de prova, por exemplo Isabelle e Twelf , e formas restritas de unificação de ordem superior (unificação de padrão de ordem superior ) são usadas em algumas implementações de linguagem de programação, como lambdaProlog , pois os padrões de ordem superior são expressivos , ainda assim, seu procedimento de unificação associado retém propriedades teóricas mais próximas da unificação de primeira ordem.

Definições formais comuns

Pré-requisitos

Formalmente, uma abordagem de unificação pressupõe

• Um conjunto infinito de variáveis . Para unificação de ordem superior, é conveniente escolher disjunto do conjunto de variáveis ​​de limite de termo lambda .${\ displaystyle V}$${\ displaystyle V}$
• Um conjunto de termos como esse . Para unificação de primeira ordem e unificação de ordem superior, geralmente é o conjunto de termos de primeira ordem (termos construídos a partir de símbolos de variáveis ​​e funções) e termos lambda (termos contendo algumas variáveis ​​de ordem superior), respectivamente.${\ displaystyle T}$${\ displaystyle V \ subseteq T}$${\ displaystyle T}$
• Um mapeamento vars : , atribuindo a cada termo o conjunto de variáveis livres que ocorrem em .${\ displaystyle T \ rightarrow}$ ${\ displaystyle \ mathbb {P}}$${\ displaystyle (V)}$${\ displaystyle t}$${\ displaystyle {\ text {vars}} (t) \ subsetneq V}$${\ displaystyle t}$
• Uma relação de equivalência em , indicando que os termos são considerados iguais. Para unificação de ordem superior, geralmente se e são equivalentes alfa . Para a unificação E de primeira ordem, reflete o conhecimento prévio sobre certos símbolos de função; por exemplo, se é considerado comutativo, se resulta da troca dos argumentos de algumas (possivelmente todas) ocorrências. Se não houver nenhum conhecimento prévio, apenas literal ou sintaticamente os termos idênticos são considerados iguais; neste caso, ≡ é chamada de teoria livre (porque é um objeto livre ), a teoria vazia (porque o conjunto de sentenças equacionais , ou o conhecimento de fundo, está vazio), a teoria das funções não interpretadas (porque a unificação é feita em termos não interpretados ) ou a teoria dos construtores (porque todos os símbolos de função apenas criam termos de dados, em vez de operar sobre eles).${\ displaystyle \ equiv}$${\ displaystyle T}$${\ displaystyle t \ equiv u}$${\ displaystyle t}$${\ displaystyle u}$${\ displaystyle \ equiv}$${\ displaystyle \ oplus}$${\ displaystyle t \ equiv u}$${\ displaystyle u}$${\ displaystyle t}$${\ displaystyle \ oplus}$

Termo de primeira ordem

Dado um conjunto de símbolos variáveis, um conjunto de símbolos constantes e conjuntos de símbolos de função n -ary, também chamados de símbolos de operador, para cada número natural , o conjunto de termos (não classificados de primeira ordem) é definido recursivamente para ser o menor conjunto com as seguintes propriedades: ${\ displaystyle V}$${\ displaystyle C}$${\ displaystyle F_ {n}}$${\ displaystyle n \ geq 1}$${\ displaystyle T}$

• cada símbolo variável é um termo: ,${\ displaystyle V \ subseteq T}$
• cada símbolo constante é um termo: ,${\ displaystyle C \ subseteq T}$
• a partir de cada n termos e de cada símbolo de função n -ary , um termo maior pode ser construído.${\ displaystyle t_ {1}, ... t_ {n}}$${\ displaystyle f \ in F_ {n}}$${\ displaystyle f (t_ {1}, ..., t_ {n})}$

Por exemplo, se é um símbolo de variável, é um símbolo de constante e é um símbolo de função binária, então , e (portanto) pela primeira, segunda e terceira regra de construção de termos, respectivamente. O último termo é geralmente escrito como , usando notação de infixo e o símbolo de operador mais comum + por conveniência. ${\ displaystyle x \ in V}$${\ displaystyle 1 \ in C}$${\ displaystyle {\ text {add}} \ in F_ {2}}$${\ displaystyle x \ in T, 1 \ in T}$${\ displaystyle {\ text {add}} (x, 1) \ in T}$${\ displaystyle x + 1}$

Termo de ordem superior

Substituição

Uma substituição é um mapeamento de variáveis ​​para termos; a notação se refere a um mapeamento de substituição de cada variável para o termo , para e todas as outras variáveis ​​para si mesmo. A aplicação dessa substituição a um termo é escrita em notação pós-fixada como ; significa (simultaneamente) substituir todas as ocorrências de cada variável no termo por . O resultado da aplicação de uma substituição a um termo é chamado de instância desse termo . Como um exemplo de primeira ordem, aplicando a substituição { x ↦ h ( a , y ), z ↦ b } ao termo ${\ displaystyle \ sigma: V \ rightarrow T}$${\ displaystyle \ {x_ {1} \ mapsto t_ {1}, ..., x_ {k} \ mapsto t_ {k} \}}$${\ displaystyle x_ {i}}$${\ displaystyle t_ {i}}$${\ displaystyle i = 1, ..., k}$${\ displaystyle t}$${\ displaystyle t \ {x_ {1} \ mapsto t_ {1}, ..., x_ {k} \ mapsto t_ {k} \}}$${\ displaystyle x_ {i}}$${\ displaystyle t}$${\ displaystyle t_ {i}}$${\ displaystyle t \ tau}$${\ displaystyle \ tau}$${\ displaystyle t}$${\ displaystyle t}$

	${\ displaystyle f (}$	${\ displaystyle {\ textbf {x}}}$	${\ displaystyle, a, g (}$	${\ displaystyle {\ textbf {z}}}$	${\ displaystyle), y)}$
rendimentos
	${\ displaystyle f (}$	${\ displaystyle {\ textbf {h}} ({\ textbf {a}}, {\ textbf {y}})}$	${\ displaystyle, a, g (}$	${\ displaystyle {\ textbf {b}}}$	${\ displaystyle), y).}$

Generalização, especialização

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

Se ≡ for identidade literal (sintática) de termos, um termo pode ser mais geral e mais especial do que outro somente se ambos os termos diferirem apenas em seus nomes de variáveis, não em sua estrutura sintática; tais termos são chamados de variantes ou renomeações uns dos outros. Por exemplo, é uma variante de , uma vez que ${\ displaystyle f (x_ {1}, a, g (z_ {1}), y_ {1})}$${\ displaystyle f (x_ {2}, a, g (z_ {2}), y_ {2})}$

e

No entanto, não é uma variante de , uma vez que nenhuma substituição pode transformar o último termo no primeiro. O último termo é, portanto, apropriadamente mais especial do que o anterior. ${\ displaystyle f (x_ {1}, a, g (z_ {1}), y_ {1})}$${\ displaystyle f (x_ {2}, a, g (x_ {2}), x_ {2})}$

Para arbitrário , um termo pode ser mais geral e mais especial do que um termo estruturalmente diferente. Por exemplo, se ⊕ for idempotente , ou seja, se sempre , o termo é mais geral do que , e vice-versa, embora e sejam de estrutura diferente. ${\ displaystyle \ equiv}$${\ displaystyle x \ oplus x \ equiv x}$${\ displaystyle x \ oplus y}$${\ displaystyle z}$${\ displaystyle x \ oplus y}$${\ displaystyle z}$

Uma substituição é mais especial do que, ou subsumida por, uma substituição se for mais especial do que para cada termo . Também dizemos que é mais geral do que . Por exemplo, é mais especial do que , mas não é, pois não é mais especial do que . ${\ displaystyle \ sigma}$${\ displaystyle \ tau}$${\ displaystyle t \ sigma}$${\ displaystyle t \ tau}$${\ displaystyle t}$${\ displaystyle \ tau}$${\ displaystyle \ sigma}$${\ displaystyle \ {x \ mapsto a, y \ mapsto a \}}$${\ displaystyle \ tau = \ {x \ mapsto y \}}$${\ displaystyle \ sigma = \ {x \ mapsto a \}}$${\ displaystyle f (x, y) \ sigma = f (a, y)}$${\ displaystyle f (x, y) \ tau = f (y, y)}$

Problema de unificação, conjunto de soluções

Um problema 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 . Essa substituição também é chamada de unificador do problema da 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. ${\ displaystyle i = 1, ..., n}$

Para um dado problema de unificação, um conjunto S de unificadores é denominado completo se cada substituição de solução é subsumida por alguma substituição σ ∈ S ; o conjunto S é denominado mínimo se nenhum de seus membros inclui outro.

Unificação sintática de termos de primeira ordem

Diagrama de triângulo esquemático de termos unificando sintaticamente t ₁ e t ₂ por uma substituição σ

A unificação sintática de termos de primeira ordem é a estrutura de unificação mais amplamente usada. Baseia-se em T sendo o conjunto de termos de primeira ordem (sobre um determinado conjunto V de variáveis, C de constantes e F _n de símbolos de função n -ary) e em ≡ sendo igualdade sintática . Nesta estrutura, cada problema de unificação solucionável { l ₁ ≐ r ₁ , ..., l _n ≐ r _n } tem um conjunto de soluções singleton completo e obviamente mínimo { σ } . Seu membro σ é chamado de unificador mais geral ( mgu ) do problema. Os termos nos lados esquerdo e direito de cada equação potencial tornam-se sintaticamente iguais quando o mgu é aplicado, isto é, l ₁ σ = r ₁ σ ∧ ... ∧ l _n σ = r _n σ . Qualquer unificador do problema é subsumido pelo mgu σ . O mgu é único até as variantes: se S ₁ e S ₂ são conjuntos de soluções completas e mínimas do mesmo problema de unificação sintática, então S ₁ = { σ ₁ } e S ₂ = { σ ₂ } para algumas substituições σ ₁ e σ ₂ , e xσ ₁ é uma variante do xσ ₂ para cada uma das variáveis X que ocorre no problema.

Por exemplo, o problema de 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 )}	.

Este também é o unificador mais geral. Outros unificadores para o mesmo problema são, por exemplo, { 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 infinitamente muitos unificadores semelhantes.

Como outro exemplo, o problema g ( x , x ) ≐ f ( y ) não tem solução com respeito a ≡ ser identidade literal, uma vez que qualquer substituição aplicada ao lado esquerdo e direito manterá o g e f mais externo , respectivamente, e termos com diferentes símbolos de função externa são sintaticamente diferentes.

Um algoritmo de unificação

O primeiro algoritmo fornecido por Robinson (1965) era bastante ineficiente; cf. caixa. O seguinte algoritmo mais rápido originou-se de Martelli, Montanari (1982). Este artigo também lista as tentativas anteriores de encontrar um algoritmo de unificação sintática eficiente e afirma que os algoritmos de tempo linear foram descobertos de forma independente por Martelli, Montanari (1976) e Paterson, Wegman (1978).

Dado um conjunto finito de equações potenciais, o algoritmo aplica regras para transformá-lo em um conjunto equivalente de equações da forma { x ₁ ≐ u ₁ , ..., x _m ≐ u _m } onde x ₁ , ..., x _m são variáveis ​​distintas e u ₁ , ..., u _m são termos que não contêm nenhum dos x _i . Um conjunto deste formulário pode ser lido como uma substituição. Se não houver solução, o algoritmo termina com ⊥; outros autores usam "Ω", "{}" ou " reprovado " nesse caso. A operação de substituição de todas as ocorrências da variável x no problema G pelo termo t é denotada por G { x ↦ t }. Para simplificar, os símbolos constantes são considerados símbolos de função com zero argumentos. ${\ displaystyle G = \ {s_ {1} \ doteq t_ {1}, ..., s_ {n} \ doteq t_ {n} \}}$

${\ displaystyle G \ cup \ {t \ doteq t \}}$	${\ displaystyle \ Rightarrow}$	${\ displaystyle G}$		excluir
${\ displaystyle G \ cup \ {f (s_ {0}, ..., s_ {k}) \ doteq f (t_ {0}, ..., t_ {k}) \}}$	${\ displaystyle \ Rightarrow}$	${\ displaystyle G \ cup \ {s_ {0} \ doteq t_ {0}, ..., s_ {k} \ doteq t_ {k} \}}$		decompor
${\ displaystyle G \ cup \ {f (s_ {0}, \ ldots, s_ {k}) \ doteq g (t_ {0}, ..., t_ {m}) \}}$	${\ displaystyle \ Rightarrow}$	${\ displaystyle \ bot}$	se ou${\ displaystyle f \ neq g}$${\ displaystyle k \ neq m}$	conflito
${\ displaystyle G \ cup \ {f (s_ {0}, ..., s_ {k}) \ doteq x \}}$	${\ displaystyle \ Rightarrow}$	${\ displaystyle G \ cup \ {x \ doteq f (s_ {0}, ..., s_ {k}) \}}$		troca
${\ displaystyle G \ cup \ {x \ doteq t \}}$	${\ displaystyle \ Rightarrow}$	${\ displaystyle G \ {x \ mapsto t \} \ cup \ {x \ doteq t \}}$	se e${\ displaystyle x \ not \ in {\ text {vars}} (t)}$${\ displaystyle x \ in {\ text {vars}} (G)}$	eliminar
${\ displaystyle G \ cup \ {x \ doteq f (s_ {0}, ..., s_ {k}) \}}$	${\ displaystyle \ Rightarrow}$	${\ displaystyle \ bot}$	E se ${\ displaystyle x \ in {\ text {vars}} (f (s_ {0}, ..., s_ {k}))}$	Verifica

Ocorre verificação

Uma tentativa de unificar uma variável x com um termo contendo x como um subtermo estrito x ≐ f (..., x , ...) levaria a um termo infinito como solução para x , uma vez que x ocorreria como um subtermo de si mesmo . No conjunto de termos (finitos) de primeira ordem conforme definido acima, a equação x ≐ f (..., x , ...) não tem solução; portanto, a regra de eliminação só pode ser aplicada se x ∉ vars ( t ). Uma vez que essa verificação adicional, chamada de verificação ocorre , retarda o algoritmo, ela é omitida, por exemplo, na maioria dos sistemas Prolog. Do ponto de vista teórico, omitir o cheque equivale a resolver equações em árvores infinitas, veja abaixo .

Prova de rescisão

Para a prova de término do algoritmo, considere um triplo, 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ímbolos e constantes de função no lado esquerdo das equações potenciais e n _eqn é o número de equações. Quando a regra de eliminação é aplicada, n _var diminui, uma vez que x é eliminado de G e mantido apenas em { x ≐ t }. A aplicação de qualquer outra regra nunca pode aumentar n _var novamente. Quando a regra decompõe , conflito ou troca é aplicada, n _lhs diminui, já que pelo menos o f mais externo do lado esquerdo desaparece. Aplicar qualquer uma das regras restantes de exclusão ou verificação não pode aumentar n _lhs , mas diminui n _eqn . Portanto, qualquer aplicação de regra diminui o triplo em relação à ordem lexicográfica , o que só é possível um número finito de vezes. ${\ displaystyle \ langle n_ {var}, n_ {lhs}, n_ {eqn} \ rangle}$${\ displaystyle \ langle n_ {var}, n_ {lhs}, n_ {eqn} \ rangle}$

Conor McBride observa que "ao expressar a estrutura que a unificação explora" em uma linguagem com tipos dependentes como Epigram , o algoritmo de Robinson pode se tornar recursivo no número de variáveis , 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 do Prolog, um símbolo que começa com uma letra maiúscula é um nome de variável; um símbolo que começa com uma letra minúscula é um símbolo de função; a vírgula é usada como o operador lógico e . Para notação matemática, x, y, z são usados ​​como variáveis, f, g como símbolos de função e a, b como constantes.

Notação prólogo	Notação matemática	Substituição unificadora	Explicação
a = a	{ a = a }	{}	Bem-sucedido. ( tautologia )
a = b	{ a = b }	⊥	a e b não correspondem
X = X	{ x = x }	{}	Bem-sucedido. ( tautologia )
a = X	{ a = x }	{ x ↦ a }	x é unificado com a constante a
X = Y	{ x = y }	{ x ↦ y }	x e y têm aliases
f(a,X) = f(a,b)	{ f ( a , x ) = f ( a , b )}	{ x ↦ b }	função e símbolos constantes coincidem, 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 têm aliases
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 da função f têm aridade diferente
f(g(X)) = f(Y)	{ f ( g ( x )) = f ( y )}	{ y ↦ g ( x )}	Unifica y com o termo${\ displaystyle g (x)}$
f(g(X),X) = f(Y,a)	{ f ( g ( x ), x ) = f ( y , a )}	{ x ↦ a , y ↦ g ( a )}	Unifica x com constante um , e y com o termo${\ displaystyle g (a)}$
X = f(X)	{ x = f ( x )}	deveria ser ⊥	Retorna ⊥ na lógica de primeira ordem e em muitos dialetos Prolog modernos (reforçados pela verificação de ocorrências ). É bem-sucedido no Prolog tradicional e no Prolog II, unificando x com termo infinito x=f(f(f(f(...)))).
X = Y, Y = a	{ x = y , y = a }	{ x ↦ a , y ↦ a }	Tanto x quanto y são unificados com a constante a
a = Y, X = Y	{ a = y , x = y }	{ x ↦ a , y ↦ a }	Como acima (a ordem das equações no conjunto não importa)
X = a, b = X	{ x = a , b = x }	⊥	Falha. a e b não correspondem, de modo que x não pode ser unificado com ambos

Dois termos com uma árvore exponencialmente maior para sua instância menos comum. Sua representação dag (mais à 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 pode ter um tamanho de 2 ⁿ . Por exemplo, o problema tem o unificador mais geral , cf. foto. Para evitar complexidade de tempo exponencial causada por tal explosão, algoritmos de unificação avançados trabalham em grafos acíclicos direcionados (dags) ao invés de árvores. ${\ displaystyle (((a * z) * y) * x) * w \ doteq w * (x * (y * (z * a)))}$${\ displaystyle \ {z \ mapsto a, y \ mapsto a * a, x \ mapsto (a * a) * (a * a), w \ mapsto ((a * a) * (a * a)) * ( (a * a) * (a * a)) \}}$

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

O conceito de unificação é uma das principais ideias por trás da programação lógica , mais conhecida por meio da linguagem Prolog . Ele representa o mecanismo de vinculação do conteúdo de variáveis ​​e pode ser visto como um tipo de atribuição única. No Prolog, esta operação é denotada pelo símbolo de igualdade =, mas também é feita ao instanciar variáveis ​​(veja abaixo). Ele também é usado em outros idiomas pelo uso do símbolo de igualdade =, mas também em conjunto com muitas operações, incluindo +, -, *, /. Os algoritmos de inferência de tipo são normalmente baseados na unificação.

No Prolog:

1. Uma variável não instanciada - isto é, nenhuma unificação anterior foi executada nela - pode ser unificada com um átomo, um termo ou outra variável não instanciada, tornando-se assim efetivamente seu apelido. Em muitos dialetos Prolog modernos e na lógica de primeira ordem , uma variável não pode ser unificada com um termo que a contém; esta é a chamada verificação de ocorrência .
2. Dois átomos só podem ser unificados se forem idênticos.
3. Da mesma forma, um termo pode ser unificado com outro termo se os símbolos de função superior e aridades dos termos forem idênticos e se os parâmetros puderem ser unificados simultaneamente. Observe que este é um comportamento recursivo.

Aplicação: inferência de tipo

A unificação é usada durante a inferência de tipo, por exemplo, na linguagem de programação funcional Haskell . Por um lado, o programador não precisa fornecer informações de tipo para todas as funções, por outro lado, é usado para detectar erros de digitação. A expressão Haskell True : ['x', 'y', 'z']não foi digitada corretamente. A função de construção de lista (:)é do tipo a -> [a] -> [a]e, para o primeiro argumento, Truea variável de tipo polimórfico adeve ser unificada com Trueo tipo de Bool,. O segundo argumento, ['x', 'y', 'z']é do tipo [Char], mas anão pode ser ao mesmo tempo Boole Char, ao mesmo tempo.

Como para Prolog, um algoritmo para inferência de tipo pode ser fornecido:

1. Qualquer variável de tipo unifica-se com qualquer expressão de tipo e é instanciada para essa expressão. Uma teoria específica pode restringir esta regra com uma verificação de ocorrência.
2. Duas constantes de tipo se unificam apenas se forem do mesmo tipo.
3. Duas construções de tipo unificam apenas se forem aplicativos do mesmo construtor de tipo e todos os seus tipos de componente se unificar recursivamente.

Devido à sua natureza declarativa, a ordem em uma sequência de unificações (geralmente) não é importante.

Observe que, na terminologia da lógica de primeira ordem , um átomo é uma proposição básica e é unificado de forma semelhante a um termo Prolog.

Unificação ordenada por ordem

A lógica de ordenação permite atribuir uma classificação , ou tipo , a cada termo e declarar uma classificação s ₁ uma subclassificação de outra classificação s ₂ , comumente escrita como s ₁ ⊆ s ₂ . Por exemplo, ao refletir sobre criaturas biológicas, é útil declarar um cão de classificaçãocomo uma subclasse de uma espécie de animal . Sempre que um termo de algum tipo s é necessário, um termo de qualquer subconjunto de s pode ser fornecido em seu lugar. Por exemplo, assumindo uma declaração de função mãe : animal → animal , e uma declaração constante lassie : cachorro , o termo mãe ( moça ) é perfeitamente válido e tem o tipo animal . Para fornecer a informação de que a mãe de um cão é por sua vez um cão, pode ser emitidaoutra declaração mãe : cão → cão ; isso é chamado de sobrecarga de função , semelhante à sobrecarga em linguagens de programação .

Walther deu um algoritmo de unificação de termos na lógica fim-ordenada, exigindo para quaisquer dois tipos declarados s ₁ , s ₂ a sua intersecção s ₁ ∩ s ₂ a ser declarada, também: se x ₁ e x ₂ é uma variável do tipo s ₁ e s ₂ , respectivamente, a equação x ₁ ≐ x ₂ tem a solução { x ₁ = x , x ₂ = x }, onde x : s ₁ ∩ s ₂ . Depois de incorporar este algoritmo em um provador de teoremas automatizado baseado em cláusulas, ele poderia resolver um problema de benchmark traduzindo-o em lógica ordenada, assim reduzindo-o a uma ordem de magnitude, conforme muitos predicados unários se transformavam em tipos.

Smolka generalizou a lógica ordenada para permitir o polimorfismo paramétrico . Em sua estrutura, as declarações de subclassificação são propagadas para expressões de tipo complexo. Como um exemplo de programação, uma lista de classificação paramétrica ( X ) pode ser declarada (com X sendo um parâmetro de tipo como em um modelo C ++ ), e de uma declaração de subsorte int ⊆ float a lista de relação ( int ) ⊆ lista ( float ) é automaticamente inferida, o que significa que cada lista de inteiros também é uma lista de floats.

Schmidt-Schauß generalizou a lógica ordenada para permitir declarações de termos. Como exemplo, assumindo declarações de subclassificação par ⊆ int e ímpar ⊆ int , uma declaração de termo como ∀ i  : int . ( i + i ): permite ainda declarar uma propriedade de adição inteira que não poderia ser expressa por sobrecarga comum.

Unificação de termos infinitos

Plano de fundo em árvores infinitas:

• B. Courcelle (1983). "Propriedades Fundamentais das Árvores Infinitas" (PDF) . Theoret. Comput. Sci . 25 (2): 95–169. doi : 10.1016 / 0304-3975 (83) 90059-2 . Arquivo do original (PDF) em 21/04/2014 . Página visitada em 28/06/2013 .
• Michael J. Maher (julho de 1988). "Axiomatizações Completas das Álgebras de Árvores Finitas, Racionais e Infinitas". Proc. IEEE 3rd Annual Symp. on Logic in Computer Science, Edimburgo . pp. 348–357.
• Joxan Jaffar; Peter J. Stuckey (1986). "Semântica de Programação Lógica de Árvore Infinita" . Ciência da Computação Teórica . 46 : 141–158. doi : 10.1016 / 0304-3975 (86) 90027-7 .

Algoritmo de unificação, Prolog II:

• A. Colmerauer (1982). KL Clark; S.-A. Tarnlund (eds.). Árvores Prolog e Infinitas . Academic Press.
• Alain Colmerauer (1984). "Equações e Inequações em Árvores Finitas e Infinitas". Em ICOT (ed.). Proc. Int. Conf. em sistemas de computador de quinta geração . pp. 85–99.

Formulários:

• Francis Giannesini; Jacques Cohen (1984). "Parser Generation and Grammar Manipulation using Prolog's Infinite Trees" . Journal of Logic Programming . 1 (3): 253–265. doi : 10.1016 / 0743-1066 (84) 90013-X .

E-unificação

E-unificação é o problema de encontrar soluções para um determinado conjunto de equações , tendo em conta alguns equational conhecimento de fundo E . O último é dado como um conjunto de igualdades universais . Para alguns conjuntos específicos E , algoritmos de resolução de equações (também conhecidos como algoritmos de unificação E ) foram desenvolvidos; para outros, foi provado que nenhum desses algoritmos pode existir.

Por exemplo, se um e b são constantes distintas, a equação não tem uma solução no que diz respeito ao puramente unificação sintática , onde nada se sabe sobre o operador . No entanto, se o é conhecido como comutativo , então a substituição { x ↦ b , y ↦ a } resolve a equação acima, uma vez que ${\ displaystyle x * a \ doteq y * b}$${\ displaystyle *}$${\ displaystyle *}$

	${\ displaystyle x * a}$	{ x ↦ b , y ↦ a }
=	${\ displaystyle b * a}$		por aplicação de substituição
=	${\ displaystyle a * b}$		por comutatividade de ${\ displaystyle *}$
=	${\ displaystyle y * b}$	{ x ↦ b , y ↦ a }	por aplicação de substituição (inversa)

O conhecimento de fundo E poderia indicar a comutatividade de pela igualdade universal " para todos u , v ". ${\ displaystyle *}$${\ displaystyle u * v = v * u}$

Conjunto de conhecimentos básicos específicos E

Usou convenções de nomenclatura

∀ u , v , w :	${\ displaystyle u * (v * w)}$	=	${\ displaystyle (u * v) * w}$	UMA	Associatividade de ${\ displaystyle *}$
∀ u , v :	${\ displaystyle u * v}$	=	${\ displaystyle v * u}$	C	Comutatividade de ${\ displaystyle *}$
∀ u , v , w :	${\ displaystyle u * (v + w)}$	=	${\ displaystyle u * v + u * w}$	D l	Distributividade esquerda de mais${\ displaystyle *}$${\ displaystyle +}$
∀ u , v , w :	${\ displaystyle (v + w) * u}$	=	${\ displaystyle v * u + w * u}$	D r	Distributividade certa de mais${\ displaystyle *}$${\ displaystyle +}$
∀ u :	${\ displaystyle u * u}$	=	você	eu	Idempotência de ${\ displaystyle *}$
∀ u :	${\ displaystyle n * u}$	=	você	N l	Elemento neutro esquerdo n em relação a${\ displaystyle *}$
∀ u :	${\ displaystyle u * n}$	=	você	N r	Elemento neutro direito n com respeito a${\ displaystyle *}$

Diz-se que a unificação é decidível para uma teoria, se um algoritmo de unificação foi desenvolvido para ela que termina para qualquer problema de entrada. Diz-se que a unificação é semidecidível para uma teoria, se um algoritmo de unificação foi desenvolvido para ela que termina para qualquer problema de entrada solucionável , mas pode continuar procurando para sempre por soluções de um problema de entrada insolúvel.

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

• UMA
• A , C
• A , C , I
• A , C , N _l
• A , eu
• A , N _l , N _r (monóide)
• C
• Anéis booleanos
• Grupos abelianos , mesmo se a assinatura for expandida por símbolos adicionais arbitrários (mas não axiomas)
• Álgebras modais K4

A unificação é semidecidível para as seguintes teorias:

• A , D _l , D _r
• A , C , D _l
• Anéis comutativos

Paramodulação unilateral

Se houver um sistema de reescrita de termo convergente R disponível para E , o algoritmo de paramodulação unilateral pode ser usado para enumerar todas as soluções de determinadas equações.

Começando com G sendo o problema de unificação a ser resolvido e S sendo a substituição de identidade, as regras são aplicadas de forma não determinística até que o conjunto vazio apareça como o G real , caso em que o S real é uma substituição unificadora. Dependendo do fim das regras paramodulation são aplicadas, sobre a escolha da equação real a partir de L , e sobre a escolha de R ' regras s em mutação , diferentes caminhos computações são possíveis. Apenas alguns levam a uma solução, enquanto outros terminam em um G ≠ {} onde nenhuma regra adicional é aplicável (por exemplo, G = { f (...) ≐ g (...)}).

Por exemplo, um termo sistema de reescrita R é usado definindo o operador de acréscimo de listas construídas a partir de cons e nil ; onde cons ( x , y ) é escrito em notação infixa como x . y por brevidade; por exemplo, app ( a . b . nulo , c . d . nulo ) → a . app ( b . nulo , c . d . nulo ) → a . b . app ( nulo , c . d . nulo ) → a . b . c . d . nil demonstra a concatenação das listas a . b . nulo e c . d . nil , empregando a regra de reescrita 2,2, e 1. A teoria equacional E correspondente a R é o fechamento de congruência de R , ambos vistos como relações binárias em termos. Por exemplo, app ( a . B . Nula , c . D . Nil ) ≡ um . b . c . d . nulo ≡ app ( a . b . c . d . nulo , nulo ). O algoritmo paramodulation enumera soluções para as equações com respeito ao que E , quando alimentado com o exemplo I .

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 conflitos de nomes de variáveis, as regras de reescrita são renomeadas consistentemente todas as vezes antes de serem usadas por mutação de regra ; v ₂ , v ₃ , ... são nomes de variáveis ​​gerados por computador para esse propósito. Em cada linha, a equação escolhida de G é destacada em vermelho. Cada vez que a regra de mutação é aplicada, a regra de reescrita escolhida ( 1 ou 2 ) é indicada entre parênteses. Da última linha, a substituição unificadora S = { y ↦ nil , x ↦ a . nil } pode ser obtido. Na verdade, app ( x , app ( y , x )) { y ↦ nil , x ↦ a . nil } = app ( a . nil , app ( nil , a . nil )) ≡ app ( a . nil , a . nil ) ≡ a . app ( nulo , a . nulo ) ≡ a . a . nil resolve o problema fornecido. Um segundo caminho de computação bem-sucedido, obtido escolhendo "mutate (1), mutate (2), mutate (2), mutate (1)" leva à substituição S = { y ↦ a . a . nulo , x ↦ nulo }; não é mostrado aqui. Nenhum outro caminho leva ao sucesso.

Estreitando

Diagrama de triângulo da etapa de estreitamento s ↝ t na posição p no termo s , com substituição unificadora σ (linha inferior), usando uma regra de reescrita l → r (linha superior)

Se R é um sistema de reescrita de termo convergente para E , uma alternativa de abordagem à seção anterior consiste na aplicação sucessiva de " etapas de estreitamento "; isso irá eventualmente enumerar todas as soluções de uma dada equação. Uma etapa de estreitamento (cf. imagem) consiste em

• escolher um subtermo não variável do termo atual,
• unificando sintaticamente com o lado esquerdo de uma regra de R , e
• substituindo o lado direito da regra instanciada no termo instanciado.

Formalmente, se l → r é uma cópia renomeada de uma regra de reescrita de R , não tendo variáveis ​​em comum com um termo s , e o subtermo s | _p não é uma variável e é unificável com l via mgu σ , então s pode ser reduzido ao termo t = sσ [ rσ ] _p , ou seja, ao termo sσ , com o subtermo em p substituído por rσ . A situação em que s pode ser reduzida a t é comumente denotada como s ↝ t . Intuitivamente, uma sequência de etapas de estreitamento t ₁ ↝ t ₂ ↝ ... ↝ t _n pode ser pensada como uma sequência de etapas de reescrita t ₁ → t ₂ → ... → t _n , mas com o termo inicial t ₁ sendo cada vez mais instanciado, conforme necessário para tornar cada uma das regras utilizadas aplicável.

O cálculo de paramodulação do exemplo acima corresponde à seguinte sequência de estreitamento ("↓" indicando instanciação aqui):

O último termo, v ₂ . v ₂ . nil pode ser sintaticamente unificado com o termo original do lado direito a . a . nulo .

O lema de estreitamento garante que sempre que uma instância de um termo s pode ser reescrito para um termo t por um sistema de reescrita de termo convergente, então s e t podem ser estreitados e reescritos para um termo s ′ e t ′ , respectivamente, de modo que t ′ é uma instância de s ′ .

Formalmente: sempre que sσ →∗ t vale para alguma substituição σ, então existem termos s ′ , t ′ tais que s ↝∗ s ′ e t →∗ t ' e s ' τ = t ' para alguns τ substituição.

Unificação de ordem superior

Muitos aplicativos requerem que se considere a unificação de termos lambda digitados em vez de termos de primeira ordem. Essa unificação é freqüentemente chamada de unificação de ordem superior . Um ramo bem estudado da unificação de ordem superior é o problema de unificar termos lambda simplesmente digitados modulo a igualdade determinada por conversões αβη. Esses problemas de unificação não têm os unificadores mais gerais. Enquanto a unificação de ordem superior é indecidível , Gérard Huet deu um algoritmo de unificação semidecidível (pré-) que permite uma busca sistemática do espaço de unificadores (generalizando o algoritmo de unificação de Martelli-Montanari com regras para termos contendo variáveis ​​de ordem superior) que parece funcionar suficientemente bem na prática. Huet e Gilles Dowek escreveram artigos sobre esse tópico.

Dale Miller descreveu o que agora é chamado de unificação de padrões de ordem superior . Este subconjunto de unificação de ordem superior é decidível e os problemas de unificação solucionáveis ​​têm unificadores mais gerais. Muitos sistemas de computador que contêm unificação de ordem superior, como as linguagens de programação lógica de ordem superior λProlog e Twelf , geralmente implementam apenas o fragmento de padrão e não a unificação completa de ordem superior.

Na linguística computacional, uma das teorias mais influentes da elipse é que as elipses são representadas por variáveis ​​livres cujos valores são então determinados usando a Unificação de Ordem Superior (HOU). Por exemplo, a representação semântica de "Jon gosta de Mary e Peter também" é como ( j , m ) ∧ R ( p ) e o valor de R (a representação semântica da elipse) é determinado pela equação como ( j , m ) = R ( j ) . O processo de resolução de tais equações é chamado de Unificação de Ordem Superior.

Por 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 ordem superior e da unificação E, ou seja, um algoritmo para unificar o módulo de termos lambda e uma teoria equacional.

Veja também

• Reescrevendo
• Regra admissível
• Substituição explícita no cálculo lambda
• Resolução de equações matemáticas
• Desunificação : resolvendo inequações entre expressões simbólicas
• Anti-unificação : computando uma generalização menos geral (lgg) de dois termos, dual para computar uma instância mais geral (mgu)
• Alinhamento de ontologia (usar unificação com equivalência semântica )

Notas

Referências

Leitura adicional

• Franz Baader e Wayne Snyder (2001). "Teoria da Unificação" Arquivada em 08/06/2015 na Wayback Machine . Em John Alan Robinson e Andrei Voronkov , editores, Handbook of Automated Reasoning , volume I, páginas 447-533. Editores da Elsevier Science.
• Gilles Dowek (2001). "Unificação e correspondência de ordem superior" . Em Handbook of Automated Reasoning .
• Franz Baader e Tobias Nipkow (1998). Reescrita de termos e tudo isso . Cambridge University Press.
• Franz Baader e Jörg H. Siekmann  [ de ] (1993). "Teoria da Unificação". Em Handbook of Logic in Artificial Intelligence and Logic Programming .
• Jean-Pierre Jouannaud e Claude Kirchner (1991). "Resolvendo Equações em Álgebras Abstratas: Uma Pesquisa Baseada em Regras de Unificação". In Computational Logic: Essays in Honor of Alan Robinson .
• Nachum Dershowitz e Jean-Pierre Jouannaud , Rewrite Systems , em: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science , volume B Formal Models and Semantics , Elsevier, 1990, pp. 243–320
• Jörg H. Siekmann (1990). "Teoria da Unificação". Em Claude Kirchner (editor) Unificação . Academic Press.
• Kevin Knight (março de 1989). "Unificação: Uma Pesquisa Multidisciplinar" (PDF) . Pesquisas de computação ACM . 21 (1): 93–124. CiteSeerX  10.1.1.64.8967 . doi : 10.1145 / 62029.62030 . S2CID  14619034 .
• Gérard Huet e Derek C. Oppen (1980). "Equações e regras de reescrita: uma pesquisa" . Relatório técnico. Universidade de Stanford.
• Raulefs, Peter; Siekmann, Jörg; Szabó, P .; Unvericht, E. (1979). “Uma breve pesquisa sobre o estado da arte em problemas de correspondência e unificação”. Boletim ACM SIGSAM . 13 (2): 14–20. doi : 10.1145 / 1089208.1089210 . S2CID  17033087 .
• Claude Kirchner e Hélène Kirchner. Reescrevendo, resolvendo, provando . Em preparação.