Unificación (informática)

En lógica e informática , la unificación es un proceso algorítmico de resolución de ecuaciones entre expresiones simbólicas .

Dependiendo de qué expresiones (también llamadas términos ) pueden ocurrir en un conjunto de ecuaciones (también llamado problema de unificación ), y qué expresiones se consideran iguales, se distinguen varios marcos de unificación. Si en una expresión se permiten variables de orden superior, es decir, variables que representan funciones , el proceso se denomina unificación de orden superior , de lo contrario unificación de primer orden . Si se requiere una solución para hacer que ambos lados de cada ecuación sean literalmente iguales, el proceso se llama unificación sintáctica o libre , de lo contrario unificación semántica o ecuacional , o unificación E, o teoría del módulo de unificación .

La solución de un problema de unificación se denota como una sustitución , es decir, un mapeo que asigna un valor simbólico a cada variable de las expresiones del problema. Un algoritmo de unificación debe calcular para un problema dado un conjunto de sustitución mínimo y completo , es decir, un conjunto que cubra todas sus soluciones y no contenga miembros redundantes. Dependiendo del marco, un conjunto de sustitución mínimo y completo puede tener como máximo uno, como mucho un número finito, o posiblemente un número infinito de miembros, o puede que no exista en absoluto. ^{[nota 1] [1]} En algunos marcos, generalmente es imposible decidir si existe alguna solución. Para la unificación sintáctica de primer orden, Martelli y Montanari ^[2]proporcionó un algoritmo que informa la insolubilidad o calcula un conjunto de sustitución de singleton mínimo y completo que contiene el llamado unificador más general .

Por ejemplo, usando x , y , z como variables, el conjunto de ecuaciones singleton { cons ( x , cons ( x , nil )) = cons (2, y )} es un problema de unificación sintáctica de primer orden que tiene la sustitución { x ↦ 2, y ↦ cons (2, nil )} como su única solución. El problema de unificación sintáctica de primer orden { y = cons (2, y )} no tiene solución sobre el conjunto de términos finitos ; sin embargo, tiene la única solución {y ↦ cons (2, cons (2, cons (2, ...)))} sobre el conjunto de árboles infinitos . El problema de unificación semántica de primer orden { a ⋅ x = x ⋅ a } tiene cada sustitución de la forma { x ↦ a ⋅ ... ⋅ a } como una solución en un semigrupo , es decir, si (⋅) se considera asociativo ; el mismo problema, visto en un grupo abeliano , donde (⋅) se considera también conmutativo , tiene alguna sustitución como solución. El conjunto singleton { a = y( x )} es un problema de unificación sintáctica de segundo orden, ya que y es una variable de función. Una solución es { x ↦ a , y ↦ ( función de identidad )}; otro es { y ↦ ( función constante que asigna cada valor a a ), x ↦ (cualquier valor) }.

Un algoritmo de unificación fue descubierto por primera vez por Jacques Herbrand , ^{[3] [4] [5]} mientras que una primera investigación formal puede atribuirse a John Alan Robinson , ^{[6] [7]} quien usó la unificación sintáctica de primer orden como un bloque de construcción básico de su procedimiento de resolución para la lógica de primer orden, un gran paso adelante en la tecnología de razonamiento automatizado , ya que eliminó una fuente de explosión combinatoria: la búsqueda de la instanciación de términos. Hoy en día, el razonamiento automatizado sigue siendo la principal área de aplicación de la unificación. La unificación sintáctica de primer orden se utiliza en la programación lógica y en el sistema de tipo de lenguaje de programación.implementación, especialmente en algoritmos de inferencia de tipos basados en Hindley-Milner . La unificación semántica se utiliza en solucionadores SMT , algoritmos de reescritura de términos y análisis de protocolos criptográficos . La unificación de orden superior se usa en asistentes de prueba, por ejemplo Isabelle y Twelf , y las formas restringidas de unificación de orden superior (unificación de patrones de orden superior ) se usan en algunas implementaciones de lenguaje de programación, como lambdaProlog , ya que los patrones de orden superior son expresivos , sin embargo, su procedimiento de unificación asociado conserva propiedades teóricas más cercanas a la unificación de primer orden.

Definiciones formales comunes

Prerrequisitos

Formalmente, un enfoque de unificación presupone

• Un conjunto infinito de variables . Para la unificación de orden superior, es conveniente elegir disjunto del conjunto de variables enlazadas de término lambda .${\displaystyle V}$${\displaystyle V}$
• Un conjunto de términos tales que . Para la unificación de primer orden y la unificación de orden superior, suele ser el conjunto de términos de primer orden (términos construidos a partir de símbolos de función y variable) y términos lambda (términos que contienen algunas variables de orden superior), respectivamente.${\displaystyle T}$${\displaystyle V\subseteq T}$${\displaystyle T}$
• Un mapeo vars : asigna a cada término el conjunto de variables libres que ocurren en .${\displaystyle T\rightarrow }$ PAG {\ Displaystyle \ mathbb {P}} ${\displaystyle (V)}$${\displaystyle t}$${\displaystyle {\text{vars}}(t)\subsetneq V}$${\displaystyle t}$
• Una relación de equivalencia en , que indica qué términos se consideran iguales. Para la unificación de orden superior, normalmente si y son equivalentes alfa . Para la unificación E de primer orden, refleja el conocimiento previo sobre ciertos símbolos de función; por ejemplo, si se considera conmutativo, si resulta de intercambiar los argumentos de en algunas (posiblemente todas) las apariciones. ^{[nota 2]} Si no hay ningún conocimiento previo, entonces sólo literal o sintácticamente, los términos idénticos se consideran iguales; en este caso, ≡ se llama teoría libre (porque es un objeto libre ), la${\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 }$teoría vacía (porque el conjunto de oraciones de ecuaciones, o el conocimiento previo, está vacío), la teoría de funciones no interpretadas (porque la unificación se realiza en términos no interpretados), o la teoría de constructores (porque todos los símbolos de función simplemente construyen términos de datos, en lugar de operar sobre ellos).

Término de primer orden

Artículo principal: Término (lógica)

Dado un conjunto de símbolos variables, un conjunto de símbolos constantes y conjuntos de n símbolos de función aria, también llamados símbolos de operador, para cada número natural , el conjunto de términos (de primer orden sin clasificar) se define recursivamente como el conjunto más pequeño con las siguientes propiedades: ^[8]${\displaystyle V}$${\displaystyle C}$${\displaystyle F_{n}}$${\displaystyle n\geq 1}$${\displaystyle T}$

• cada símbolo de la variable es un término: ,${\displaystyle V\subseteq T}$
• cada símbolo constante es un término: ,${\displaystyle C\subseteq T}$
• a partir de cada n términos y cada símbolo de función n -aria , se puede construir un término más grande .${\displaystyle t_{1},...t_{n}}$${\displaystyle f\in F_{n}}$${\displaystyle f(t_{1},...,t_{n})}$

Por ejemplo, si es un símbolo de variable, es un símbolo de constante y es un símbolo de función binaria, entonces , y (por lo tanto) por la regla de construcción del primer, segundo y tercer término, respectivamente. El último término generalmente se escribe como , usando notación infija y el símbolo de operador más común + por conveniencia.${\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}$

Término de orden superior

Artículo principal: cálculo lambda

Sustitución

Artículo principal: Sustitución (lógica)

Una sustitución es un mapeo de variables a términos; la notación se refiere a una sustitución que asigna cada variable al término , para y todas las demás variables a sí misma. La aplicación de esa sustitución a un término se escribe en notación de sufijo como ; significa reemplazar (simultáneamente) cada ocurrencia de cada variable en el término por . El resultado de aplicar una sustitución a un término se denomina instancia de ese término . Como ejemplo de primer orden, aplicando la sustitución { x ↦ h (${\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}$a , y ), z ↦ b } al término

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

Generalización, especialización

Si un término tiene una instancia equivalente a un término , es decir, si por alguna sustitución , a continuación, se llama más general que , y se llama más especial que, o subsumido por, . Por ejemplo, es más general que si ⊕ es conmutativo , desde entonces .${\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}$

Si ≡ es una identidad literal (sintáctica) de términos, un término puede ser más general y más especial que otro solo si ambos términos difieren solo en sus nombres de variable, no en su estructura sintáctica; estos términos se denominan variantes o renombramientos entre sí. Por ejemplo, es una variante de , ya que${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$

${\displaystyle 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})}$

y

${\displaystyle 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})}$.

Sin embargo, no es una variante de , ya que ninguna sustitución puede transformar el último término en el anterior. El último término es, por tanto, propiamente más especial que el anterior.${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$

Por arbitrario , un término puede ser más general y más especial que un término estructuralmente diferente. Por ejemplo, si ⊕ es idempotente , es decir, si siempre , entonces el término es más general que , ^{[nota 3]} y viceversa, ^{[nota 4]} aunque y son de estructura diferente.${\displaystyle \equiv }$${\displaystyle x\oplus x\equiv x}$${\displaystyle x\oplus y}$${\displaystyle z}$${\displaystyle x\oplus y}$${\displaystyle z}$

Una sustitución es más especial que, o está subsumida por, una sustitución si es más especial que para cada término . También decimos que es más general que . Por ejemplo, es más especial que , pero no lo es, ya que no es más especial que . ^[9]${\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 unificación, conjunto de soluciones

Un problema de la unificación es un conjunto finito { l ₁ ≐ r ₁ , ..., l _n ≐ r _n } de ecuaciones potenciales, donde l _i , r _i ∈ T . Una sustitución σ es una solución de ese problema si l _i σ ≡ r _i σ para . Tal sustitución también se llama unificador del problema de unificación. Por ejemplo, si ⊕ es asociativo , el problema de unificación { x ⊕ a${\displaystyle i=1,...,n}$≐ a ⊕ x } tiene las soluciones { x ↦ a }, { x ↦ a ⊕ a }, { x ↦ a ⊕ a ⊕ a }, etc., mientras que el problema { x ⊕ a ≐ a } no tiene solución.

Para un problema de unificación dado, un conjunto S de unificadores se llama completo si cada sustitución de solución está subsumida por alguna sustitución σ ∈ S ; el conjunto S se llama mínimo si ninguno de sus miembros subsume a otro.

Unificación sintáctica de términos de primer orden

Diagrama de triángulo esquemático de términos unificantes sintácticamente t ₁ y t ₂ por una sustitución σ

La unificación sintáctica de términos de primer orden es el marco de unificación más utilizado. Se basa en que T es el conjunto de términos de primer orden (sobre algún conjunto V dado de variables, C de constantes y F _n de n símbolos de función aria) y en que ≡ es igualdad sintáctica . En este marco, cada problema de unificación resoluble { l ₁ ≐ r ₁ , ..., l _n ≐ r _n } tiene un conjunto de soluciones singleton completo, y obviamente mínimo, { σ} . Su miembro σ se llama el unificador más general ( mgu ) del problema. Los términos del lado izquierdo y derecho de cada ecuación potencial se vuelven sintácticamente iguales cuando se aplica mgu, es decir, l ₁ σ = r ₁ σ ∧ ... ∧ l _n σ = r _n σ . Cualquier unificador del problema es subsumido ^{[nota 5]} por mgu σ . El mgu es único hasta variantes: si S ₁ y S ₂son conjuntos de solución completa y mínima del mismo problema de unificación sintáctica, entonces S ₁ = { σ ₁ } y S ₂ = { σ ₂ } para algunas sustituciones σ ₁ y σ ₂ , y xσ ₁ es una variante de xσ ₂ para cada variable x que ocurre en el problema.

Por ejemplo, el problema de unificación { x ≐ z , y ≐ f ( x )} tiene un unificador { x ↦ z , y ↦ f ( z )}, porque

X	{ x ↦ z , y ↦ f ( z )}	=	z	=	z	{ x ↦ z , y ↦ f ( z )}	, y
y	{ x ↦ z , y ↦ f ( z )}	=	f ( z )	=	f ( x )	{ x ↦ z , y ↦ f ( z )}	.

Este es también el unificador más general. Otros unificadores para el mismo problema son, por ejemplo, { x ↦ f ( x ₁ ), y ↦ f ( f ( x ₁ )), z ↦ f ( x ₁ )}, { x ↦ f ( f ( x ₁ )), y ↦ f ( f ( f ( x ₁ ))), z ↦ f ( f ( x ₁₎)) }, etcétera; hay infinitos unificadores similares.

Como otro ejemplo, el problema g ( x , x ) ≐ f ( y ) no tiene solución con respecto a que ≡ sea identidad literal, ya que cualquier sustitución aplicada al lado izquierdo y derecho mantendrá las g y f más externas , respectivamente, y los términos con diferentes símbolos de función más externos son sintácticamente diferentes.

Un algoritmo de unificación

Algoritmo de unificación de Robinson de 1965

Los símbolos están ordenados de manera que las variables precedan a los símbolos de función. Los términos se ordenan aumentando la longitud del escrito; términos igualmente largos se ordenan lexicográficamente . ^[10] Para un conjunto T de términos, su camino de desacuerdo p es el camino lexicográficamente mínimo donde dos términos miembros de T difieren. Su conjunto de desacuerdo es el conjunto de subterráneos que comienzan en p , formalmente: { t | p  :${\displaystyle t\in T}$ }. ^[11]

Algoritmo: ^[12]

Dado un conjunto T de términos a unificar Sea inicialmente la sustitución de identidad${\displaystyle \sigma }$

hazlo para siempre si es un conjunto singleton, luego regresa fi${\displaystyle T\sigma }$ ${\displaystyle \sigma }$

sea D el conjunto de desacuerdos de sean s , t los dos términos lexicográficamente mínimos en D${\displaystyle T\sigma }$

si s no es una variable o s aparece en t entonces devuelve "NO UNIFIABLE" fi hecho${\displaystyle \sigma :=\sigma \{s\mapsto t\}}$

El primer algoritmo dado por Robinson (1965) fue bastante ineficiente; cf. caja. El siguiente algoritmo más rápido se originó en Martelli, Montanari (1982). ^{[nota 6]} Este artículo también enumera los intentos anteriores de encontrar un algoritmo de unificación sintáctica eficiente, ^{[13] [14] [15] [16] [17] [18]} y afirma que los algoritmos de tiempo lineal fueron descubiertos de forma independiente por Martelli, Montanari (1976) ^[15] y Paterson, Wegman (1978). ^{[16] [nota 7]}

Dado un conjunto finito de ecuaciones potenciales, el algoritmo aplica reglas para transformarlo en un conjunto equivalente de ecuaciones de la forma { x ₁ ≐ u ₁ , ..., x _m ≐ u _m } donde x ₁ , ..., x _m son variables distintas y u ₁ , ..., u _m son términos que no contienen ninguna de las x _i . Un conjunto de este formulario se puede leer como sustitución. Si no hay solución, el algoritmo termina con ⊥; otros autores usan "Ω", "{}" o " fail${\displaystyle G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}}$"en ese caso. La operación de sustituir todas las apariciones de la variable x en el problema G con el término t se denota G { x ↦ t }. Para simplificar, los símbolos constantes se consideran símbolos de función que tienen cero argumentos.

${\displaystyle G\cup \{t\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G}$		Eliminar
${\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}\}}$		descomponer
${\displaystyle G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	si o${\displaystyle f\neq g}$${\displaystyle k\neq m}$	conflicto
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq x\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$		intercambio
${\displaystyle G\cup \{x\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\{x\mapsto t\}\cup \{x\doteq t\}}$	si y${\displaystyle x\not \in {\text{vars}}(t)}$${\displaystyle x\in {\text{vars}}(G)}$	eliminar [nota 8]
${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	si ${\displaystyle x\in {\text{vars}}(f(s_{0},...,s_{k}))}$	cheque

Ocurre cheque

Artículo principal: Ocurre cheque

Un intento de unificar una variable x con un término que contiene x como un subtermo estricto x ≐ f (..., x , ...) conduciría a un término infinito como solución para x , ya que x ocurriría como un subtermo de sí mismo . En el conjunto de términos (finitos) de primer orden como se definió anteriormente, la ecuación x ≐ f (..., x , ...) no tiene solución; por lo tanto, la regla de eliminación solo puede aplicarse si x ∉ vars ( t ). Desde ese cheque adicional, llamado ocurre cheque, ralentiza el algoritmo, se omite, por ejemplo, en la mayoría de los sistemas Prolog. Desde un punto de vista teórico, omitir la verificación equivale a resolver ecuaciones en árboles infinitos, ver más abajo .

Comprobante de rescisión

Para la prueba de terminación del algoritmo, considere un triple donde n _var es el número de variables que ocurren más de una vez en el conjunto de ecuaciones, n _lhs es el número de símbolos de función y constantes en el lado izquierdo de las ecuaciones potenciales, y n _eqn es el número de ecuaciones. Cuando se aplica la regla eliminar , n _var disminuye, ya que x se elimina de G y se mantiene solo en { x ≐ t }. La aplicación de cualquier otra regla nunca puede volver a aumentar n _var . Cuando la regla se descompone ,${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$conflicto , o intercambio , n _lhs disminuye, ya que al menos desaparece la f más externa del lado izquierdo . La aplicación de cualquiera de las reglas restantes, eliminar o marcar , no puede aumentar n _lhs , pero disminuye n _eqn . Por tanto, cualquier aplicación de reglas disminuye el triple con respecto al orden lexicográfico , lo que es posible sólo un número finito de veces.${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$

Conor McBride observa ^[19] que "al expresar la estructura que explota la unificación" en un lenguaje de tipificación dependiente como Epigram , el algoritmo de Robinson puede volverse recursivo en el número de variables , en cuyo caso una prueba de terminación separada se vuelve innecesaria.

Ejemplos de unificación sintáctica de términos de primer orden

En la convención sintáctica de Prolog, un símbolo que comienza con una letra mayúscula es un nombre de variable; un símbolo que comienza con una letra minúscula es un símbolo de función; la coma se utiliza como operador lógico y . Para la notación matemática, x, y, z se utilizan como variables, f, g como símbolos de función y a, b como constantes.

Notación de prólogo	Notación matemática	Sustitución unificadora	Explicación
a = a	{ a = a }	{}	Tiene éxito. ( tautología )
a = b	{ a = b }	⊥	una y b no coinciden
X = X	{ x = x }	{}	Tiene éxito. ( tautología )
a = X	{ a = x }	{ x ↦ a }	x se unifica con la constante a
X = Y	{ x = y }	{ x ↦ y }	x y y son alias
f(a,X) = f(a,b)	{ f ( a , x ) = f ( a , b )}	{ x ↦ b }	los símbolos de función y constante coinciden, x se unifica con la constante b
f(a) = g(a)	{ f ( a ) = g ( a )}	⊥	f y g no coinciden
f(X) = f(Y)	{ f ( x ) = f ( y )}	{ x ↦ y }	x y y son alias
f(X) = g(Y)	{ f ( x ) = g ( y )}	⊥	f y g no coinciden
f(X) = f(Y,Z)	{ f ( x ) = f ( y , z )}	⊥	Fracasa. Los símbolos de la función f tienen diferente aridad
f(g(X)) = f(Y)	{ f ( g ( x )) = f ( y )}	{ y ↦ g ( x )}	Unifica y con el término${\displaystyle g(x)}$
f(g(X),X) = f(Y,a)	{ f ( g ( x ), x ) = f ( y , a )}	{ x ↦ a , y ↦ g ( a )}	Unifica x con constante de un , y y con el término${\displaystyle g(a)}$
X = f(X)	{ x = f ( x )}	debería ser ⊥	Devuelve ⊥ en lógica de primer orden y muchos dialectos Prolog modernos (reforzado por la comprobación de ocurre ). Triunfa en Prolog tradicional y en Prolog II, unificando x con término infinito x=f(f(f(f(...)))).
X = Y, Y = a	{ x = y , y = a }	{ x ↦ a , y ↦ a }	Tanto x como y están unificados con la constante a
a = Y, X = Y	{ a = y , x = y }	{ x ↦ a , y ↦ a }	Como arriba (el orden de las ecuaciones en el conjunto no importa)
X = a, b = X	{ x = a , b = x }	⊥	Fracasa. una y b no coinciden, por lo que x no puede ser unificado con tanto

Dos términos con un árbol exponencialmente más grande para su instancia menos común. Su representación dag (más a la derecha, parte naranja) sigue siendo de tamaño lineal.

El unificador más general de un problema de unificación sintáctica de primer orden de tamaño n puede tener un tamaño de 2 ⁿ . Por ejemplo, el problema tiene el unificador más general , cf. fotografía. Para evitar la complejidad de tiempo exponencial causada por tal explosión, los algoritmos de unificación avanzados funcionan en gráficos acíclicos dirigidos (dags) en lugar de árboles. ^[20]${\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))\}}$

Aplicación: unificación en programación lógica.

El concepto de unificación es una de las principales ideas detrás de la programación lógica , más conocida a través del lenguaje Prolog . Representa el mecanismo de vinculación del contenido de las variables y puede verse como una especie de asignación única. En Prolog, esta operación se indica con el símbolo de igualdad =, pero también se realiza al crear instancias de variables (ver más abajo). También se utiliza en otros idiomas mediante el uso del símbolo de la igualdad =, sino también en conjunción con muchas operaciones, incluyendo +, -, *, /. Los algoritmos de inferencia de tipos se basan normalmente en la unificación.

En Prolog:

1. Una variable que no está autenticada, es decir, no se realizaron unificaciones previas en ella, puede unificarse con un átomo, un término u otra variable no autenticada, convirtiéndose así efectivamente en su alias. En muchos dialectos modernos de Prolog y en la lógica de primer orden , una variable no se puede unificar con un término que la contiene; este es el llamado control de ocurre .
2. Dos átomos solo se pueden unificar si son idénticos.
3. De manera similar, un término se puede unificar con otro término si los símbolos y aridades de la función superior de los términos son idénticos y si los parámetros se pueden unificar simultáneamente. Tenga en cuenta que este es un comportamiento recursivo.

Aplicación: inferencia de tipos

La unificación se utiliza durante la inferencia de tipos, por ejemplo, en el lenguaje de programación funcional Haskell . Por un lado, el programador no necesita proporcionar información de tipo para cada función, por otro lado, se utiliza para detectar errores de escritura. La expresión de Haskell True : ['x', 'y', 'z']no está escrita correctamente. La función de lista de construcción (:)es de tipo a -> [a] -> [a], y para el primer argumento Truede la variable de tipo polimórfico atiene que ser unificado con Trueel tipo 's, Bool. El segundo argumento`` ['x', 'y', 'z']es de tipo [Char], pero ano puede ser ambos Booly Charal mismo tiempo.

Al igual que para Prolog, se puede proporcionar un algoritmo para la inferencia de tipos:

1. Cualquier variable de tipo se unifica con cualquier expresión de tipo y se instancia a esa expresión. Una teoría específica podría restringir esta regla con una verificación de ocurre.
2. Dos constantes de tipo se unifican solo si son del mismo tipo.
3. Las construcciones de dos tipos se unifican solo si son aplicaciones del mismo constructor de tipos y todos los tipos de sus componentes se unifican de forma recursiva.

Debido a su naturaleza declarativa, el orden en una secuencia de unificaciones no es (generalmente) importante.

Tenga en cuenta que en la terminología de la lógica de primer orden , un átomo es una proposición básica y está unificado de manera similar a un término Prólogo.

Unificación ordenada por orden

La lógica ordenada por orden permite asignar una ordenación o tipo a cada término y declarar una ordenación s _{1 como} un subgrupo de otra clase s ₂ , comúnmente escrito como s ₁ ⊆ s ₂ . Por ejemplo, al razonar sobre criaturas biológicas, es útil declarar que un perro tipoes un subgrupo de un animal tipo. Siempre que sea un término de algún tipo s se requiere, un término de cualquier subclasificación de s puede ser suministrado en su lugar. Por ejemplo, asumiendo una declaración de función madre : animal →animal , y una declaración constante lassie : perro , el término madre ( lassie ) es perfectamente válido y tiene el género animal . Para proporcionar la información de que la madre de un perro es un perro a su vez, se puede emitir otra declaración madre : perro → perro ; esto se llama sobrecarga de funciones , similar a la sobrecarga en los lenguajes de programación .

Walther dio un algoritmo de unificación para términos en lógica ordenada por orden, requiriendo que dos géneros declarados cualesquiera s ₁ , s ₂ también se declaren su intersección s ₁ ∩ s ₂ : si x ₁ y x ₂ es una variable de género s ₁ y s ₂ , respectivamente, la ecuación x ₁ ≐ x ₂ tiene la solución { x ₁ = x , x ₂ = x }, donde x: s ₁ ∩ s ₂ . ^[21] Después de incorporar este algoritmo en un probador de teoremas automatizado basado en cláusulas, pudo resolver un problema de referencia traduciéndolo a lógica ordenada por orden, reduciéndolo a un orden de magnitud, ya que muchos predicados unarios se convirtieron en clases.

Smolka generalizó la lógica ordenada por orden para permitir el polimorfismo paramétrico . ^[22] En su marco, las declaraciones de subgrupos se propagan a expresiones de tipos complejos. Como ejemplo de programación, se puede declarar una lista de ordenación paramétrica ( X ) (siendo X un parámetro de tipo como en una plantilla de C ++ ), y desde una declaración de subgrupo int ⊆ float la lista de relaciones ( int ) ⊆ list ( float ) es automáticamente inferido, lo que significa que cada lista de enteros es también una lista de flotantes.

Schmidt-Schauß generalizó la lógica ordenada por orden para permitir declaraciones de términos.^[23] Como ejemplo, asumiendo declaraciones de subtipo par ⊆ int e impar ⊆ int , una declaración de término como ∀ i  : int . ( i + i ): incluso permite declarar una propiedad de suma de enteros que no podría expresarse mediante una sobrecarga ordinaria.

Unificación de términos infinitos

Antecedentes sobre árboles infinitos:

• B. Courcelle (1983). "Propiedades fundamentales de árboles infinitos" (PDF) . Theoret. Computación. Sci . 25 (2): 95–169. doi : 10.1016 / 0304-3975 (83) 90059-2 . Archivado desde el original (PDF) el 21 de abril de 2014 . Consultado el 28 de junio de 2013 .
• Michael J. Maher (julio de 1988). "Axiomatizaciones completas de las álgebras de árboles finitos, racionales e infinitos". Proc. IEEE 3rd Annual Symp. sobre Lógica en Ciencias de la Computación, Edimburgo . págs. 348–357.
• Joxan Jaffar; Peter J. Stuckey (1986). "Semántica de la programación lógica de árbol infinito" . Informática Teórica . 46 : 141-158. doi : 10.1016 / 0304-3975 (86) 90027-7 .

Algoritmo de unificación, Prolog II:

• A. Colmerauer (1982). KL Clark; S.-A. Tarnlund (eds.). Prólogo y árboles infinitos . Prensa académica.
• Alain Colmerauer (1984). "Ecuaciones e inecuaciones en árboles finitos e infinitos". En ICOT (ed.). Proc. En t. Conf. sobre sistemas informáticos de quinta generación . págs. 85–99.

Aplicaciones:

• Francis Giannesini; Jacques Cohen (1984). "Generación de analizadores y manipulación de la gramática utilizando árboles infinitos de Prolog" . J. Programación lógica . 1 (3): 253–265. doi : 10.1016 / 0743-1066 (84) 90013-X .

E-unificación

E-unificación es el problema de encontrar soluciones a un determinado conjunto de ecuaciones , teniendo en cuenta un conocimiento básico ecuacional E . Este último se da como un conjunto de igualdades universales . Para algunos conjuntos E particulares , se han ideado algoritmos de resolución de ecuaciones (también conocidos como algoritmos de unificación E ); para otros, se ha demostrado que tales algoritmos no pueden existir.

Por ejemplo, si un y b son constantes distintas, la ecuación no tiene solución con respecto a puramente unificación sintáctica , donde no se sabe nada sobre el operador . Sin embargo, si se sabe que el es conmutativo , entonces la sustitución { x ↦ b , y ↦ a } resuelve la ecuación anterior, ya que${\displaystyle x*a\doteq y*b}$${\displaystyle *}$${\displaystyle *}$

	${\displaystyle x*a}$	{ x ↦ b , y ↦ a }
=	${\displaystyle b*a}$		por solicitud de sustitución
=	${\displaystyle a*b}$		por conmutatividad de ${\displaystyle *}$
=	${\displaystyle y*b}$	{ x ↦ b , y ↦ a }	por (inversa) aplicación de sustitución

El conocimiento de fondo E podría establecer la conmutatividad de por la igualdad universal " para todo u , v ".${\displaystyle *}$${\displaystyle u*v=v*u}$

Conjuntos de conocimientos previos particulares E

Convenciones de nomenclatura utilizadas

∀ u , v , w :	${\displaystyle u*(v*w)}$	=	${\displaystyle (u*v)*w}$	A	Asociatividad de ${\displaystyle *}$
∀ u , v :	${\displaystyle u*v}$	=	${\displaystyle v*u}$	C	Conmutatividad de ${\displaystyle *}$
∀ u , v , w :	${\displaystyle u*(v+w)}$	=	${\displaystyle u*v+u*w}$	D l	Distributividad izquierda de más${\displaystyle *}$${\displaystyle +}$
∀ u , v , w :	${\displaystyle (v+w)*u}$	=	${\displaystyle v*u+w*u}$	D r	Distributividad derecha de más${\displaystyle *}$${\displaystyle +}$
∀ u :	${\displaystyle u*u}$	=	tu	I	Idempotencia de ${\displaystyle *}$
∀ u :	${\displaystyle n*u}$	=	tu	N l	Elemento neutral izquierdo n con respecto a${\displaystyle *}$
∀ u :	${\displaystyle u*n}$	=	tu	N r	Elemento neutro derecho n con respecto a${\displaystyle *}$

Se dice que la unificación es decidible para una teoría, si se ha ideado un algoritmo de unificación para ella que termine con cualquier problema de entrada. Se dice que la unificación es semi-decidible para una teoría, si se ha ideado un algoritmo de unificación para ella que termina para cualquier problema de entrada resoluble , pero puede seguir buscando para siempre soluciones de un problema de entrada irresoluble.

La unificación es decidible por las siguientes teorías:

• A ^[24]
• A , C ^[25]
• A , C , I ^[26]
• A , C , N _l ^{[nota 9] [26]}
• A , yo ^[27]
• A , N _l , N _r (monoide) ^[28]
• C ^[29]
• Anillos booleanos ^{[30] [31]}
• Grupos abelianos , incluso si la firma se amplía con símbolos adicionales arbitrarios (pero no axiomas) ^[32]
• Álgebras modales K4 ^[33]

La unificación es semi-decidible para las siguientes teorías:

• A , D _l , D _r ^[34]
• A , C , D _l ^{[nota 9] [35]}
• Anillos conmutativos ^[32]

Paramodulación unilateral

Si hay un sistema de reescritura de términos convergente R disponible para E , el algoritmo de paramodulación unilateral ^[36] puede usarse para enumerar todas las soluciones de ecuaciones dadas.

Reglas de paramodulación unilaterales

G ∪ { f ( s 1 , ..., s n ) ≐ f ( t 1 , ..., t n )}	; S	⇒	G ∪ { s 1 ≐ t 1 , ..., s n ≐ t n }	; S		descomponer
G ∪ { x ≐ t }	; S	⇒	G { x ↦ t }	; S { x ↦ t } ∪ { x ↦ t }	si la variable x no ocurre en t	eliminar
G ∪ { f ( s 1 , ..., s n ) ≐ t }	; S	⇒	G ∪ { s 1 ≐ u 1 , ..., s n ≐ u n , r ≐ t }	; S	si f ( u 1 , ..., u n ) → r es una regla de R	mudar
G ∪ { f ( s 1 , ..., s n ) ≐ y }	; S	⇒	G ∪ { s 1 ≐ y 1 , ..., s n ≐ y n , y ≐ f ( y 1 , ..., y n )}	; S	si y 1 , ..., y n son nuevas variables	imitar

Comenzando con G como el problema de unificación a resolver y S como la sustitución de identidad, las reglas se aplican de forma no determinista hasta que el conjunto vacío aparece como el G real , en cuyo caso el S real es una sustitución unificadora. Dependiendo del orden en que se apliquen las reglas de paramodulación, de la elección de la ecuación real de G , y de la elección de las reglas de R en mutado , son posibles diferentes caminos de cálculo. Solo algunos conducen a una solución, mientras que otros terminan en un G ≠ {} donde no se aplica ninguna regla adicional (por ejemplo, G = { f (...) ≐ g(...)}).

Ejemplo de sistema de reescritura de término R

1	aplicación ( cero , z )	→ z
2	aplicación ( x . y , z )	→ x . aplicación ( y , z )

Por ejemplo, se utiliza un término sistema de reescritura R que define el operador de adición de listas construidas a partir de cons y nil ; donde cons ( x , y ) se escribe en notación infija como x . y por brevedad; p . ej., aplicación ( a . b . nil , c . d . nil ) → a . aplicación ( b . nil , c . d . nil ) → a. b . aplicación ( nil , c . d . nil ) → una . b . c . d . nil demuestra la concatenación de las listas a . b . cero y c . d . cero , empleando la regla de reescritura 2,2 y 1. La teoría de la ecuación E correspondiente a R es el cierre de congruencia de R , ambas vistas como relaciones binarias en términos. Por ejemplo, app (a . b . cero , c . d . cero ) ≡ a . b . c . d . nil ≡ aplicación ( a . b . c . d . nil , nil ). El algoritmo paramodulation enumera soluciones a las ecuaciones con respecto a ese E cuando son alimentados con el ejemplo R .

Un ejemplo exitoso de ruta de cálculo para el problema de unificación { app ( x , app ( y , x )) ≐ a . a . nil } se muestra a continuación. Para evitar conflictos de nombres de variables, las reglas de reescritura se renombran constantemente cada vez antes de que las use la mutación de reglas ; v ₂ , v ₃ , ... son nombres de variables generados por computadora para este propósito. En cada línea, la ecuación elegida de G está resaltada en rojo. Cada vez que se aplica la regla de mutación , la regla de reescritura elegida ( 1 o 2) se indica entre paréntesis. Desde la última línea, la sustitución unificadora S = { y ↦ nil , x ↦ a . nil } se puede obtener. De hecho, app ( x , app ( y , x )) { y ↦ nil , x ↦ a . nil } = aplicación ( a . nil , aplicación ( nil , a . nil )) ≡ aplicación ( a. cero , a . cero ) ≡ a . aplicación ( cero , a . cero ) ≡ a . a . nil resuelve el problema dado. Una segunda ruta de cálculo exitosa, que se puede obtener eligiendo "mutar (1), mutar (2), mutar (2), mutar (1)" conduce a la sustitución S = { y ↦ a . a . nulo , x ↦ nulo }; no se muestra aquí. Ningún otro camino conduce al éxito.

Ejemplo de cálculo unificador

Regla usada		GRAMO	S
		{ aplicación ( x , aplicación ( y , x )) ≐ a . a . nil }	{}
mutar (2)	⇒	{ x ≐ v 2 . v 3 , aplicación ( y , x ) ≐ v 4 , v 2 . aplicación ( v 3 , v 4 ) ≐ a . a . nil }	{}
descomponer	⇒	{ x ≐ v 2 . v 3 , aplicación ( y , x ) ≐ v 4 , v 2 ≐ a , aplicación ( v 3 , v 4 ) ≐ a . nil }	{}
eliminar	⇒	{ Aplicación ( y , v 2 . V 3 ) ≐ v 4 , v 2 ≐ una , aplicación ( v 3 , v 4 ) ≐ una . nil }	{ x ↦ v 2 . v 3 }
eliminar	⇒	{ aplicación ( y , a . v 3 ) ≐ v 4 , aplicación ( v 3 , v 4 ) ≐ a . nil }	{ x ↦ a . v 3 }
mutar (1)	⇒	{ y ≐ nil , a . v 3 ≐ v 5 , v 5 ≐ v 4 , app ( v 3 , v 4 ) ≐ a . nil }	{ x ↦ a . v 3 }
eliminar	⇒	{ y ≐ nil , a . v 3 ≐ v 4 , aplicación ( v 3 , v 4 ) ≐ a . nil }	{ x ↦ a . v 3 }
eliminar	⇒	{ a . v 3 ≐ v 4 , aplicación ( v 3 , v 4 ) ≐ a . nil }	{ y ↦ cero , x ↦ a . v 3 }
mutar (1)	⇒	{ a . v 3 ≐ v 4 , v 3 ≐ nil , v 4 ≐ v 6 , v 6 ≐ una . nil }	{ y ↦ cero , x ↦ a . v 3 }
eliminar	⇒	{ a . v 3 ≐ v 4 , v 3 ≐ nil , v 4 ≐ una . nil }	{ y ↦ cero , x ↦ a . v 3 }
eliminar	⇒	{ a . nil ≐ v 4 , v 4 ≐ una . nil }	{ y ↦ cero , x ↦ a . nil }
eliminar	⇒	{ a . nil ≐ a . nil }	{ y ↦ cero , x ↦ a . nil }
descomponer	⇒	{ a ≐ a , nil ≐ nil }	{ y ↦ cero , x ↦ a . nil }
descomponer	⇒	{ nil ≐ nil }	{ y ↦ cero , x ↦ a . nil }
descomponer	⇒	{}	{ y ↦ cero , x ↦ a . nil }

Estrechamiento

Diagrama de triángulo del paso de estrechamiento s ↝ t en la posición p en el término s , con sustitución unificadora σ (fila inferior), usando una regla de reescritura l → r (fila superior)

Si R es un sistema de reescritura de términos convergente para E , un enfoque alternativo a la sección anterior consiste en la aplicación sucesiva de " pasos de estrechamiento "; esto eventualmente enumerará todas las soluciones de una ecuación dada. Un paso de estrechamiento (ver imagen) consiste en

• eligiendo un subtermo no variable del término actual,
• unificándolo sintácticamente con el lado izquierdo de una regla de R , y
• reemplazando el lado derecho de la regla instanciada en el término instanciado.

Formalmente, si l → r es una copia renombrada de una regla de reescritura de R , que no tiene variables en común con un término s , y el subtermo s | _p no es una variable y es unificables con l a través de la MGU σ , entonces s se puede estrechan con el término t = sσ [ rσ ] _p , es decir con el término sσ , con el subtérmino en p sustituye por rσ . La situación que sse puede reducir a t se denota comúnmente como s ↝ t . Intuitivamente, una secuencia de pasos de reducción t ₁ ↝ t ₂ ↝ ... ↝ t _n se puede considerar como una secuencia de pasos de reescritura t ₁ → t ₂ → ... → t _n , pero con el término inicial t ₁ siendo más y más instanciado, según sea necesario para que cada una de las reglas utilizadas sean aplicables.

El cálculo de paramodulación del ejemplo anterior corresponde a la siguiente secuencia de estrechamiento ("↓" indica instanciación aquí):

aplicación (

X

, aplicación ( y ,

X

))

↓

↓

x ↦ v 2 . v 3

aplicación (

v 2 . v 3

, aplicación ( y ,

v 2 . v 3

))

→

v 2 . aplicación ( v 3 , aplicación (

y

, v 2 . v 3 ))

↓

y ↦ nada

v 2 . aplicación ( v 3 , aplicación (

nulo

, v 2 . v 3 ))

→

v 2 . aplicación (

v 3

, v 2 .

v 3

)

↓

↓

v 3 ↦ nada

v 2 . aplicación (

nulo

, v 2 .

nulo

)

→

v 2 . v 2 . nulo

El último término, v ₂ . v ₂ . nil se puede unificar sintácticamente con el término original del lado derecho a . a . cero .

El lema de estrechamiento ^[37] asegura que siempre que una instancia de un término s se pueda reescribir en un término t mediante un sistema de reescritura de términos convergente, entonces s y t se puedan estrechar y reescribir en un término s ′ y t ′ , respectivamente, tal que t ′ es una instancia de s ′ .

Formalmente: siempre que sσ →∗ t se cumple para alguna sustitución σ, entonces existen términos s ′ , t ′ tales que s ↝∗ s ′ y t →∗ t ′ y s ′ τ = t ′ para alguna sustitución τ.

Unificación de orden superior

Muchas aplicaciones requieren que uno considere la unificación de términos lambda escritos en lugar de términos de primer orden. Tal unificación a menudo se llama unificación de orden superior . Una rama bien estudiada de la unificación de orden superior es el problema de unificar términos lambda simplemente tipados en módulo la igualdad determinada por las conversiones αβη. Tales problemas de unificación no tienen la mayoría de los unificadores generales. Mientras que de orden superior unificación es indecidible , ^{[38] [39] [40]} Gérard Huet dio un semi-decidable algoritmo de unificación (pre-) ^[41] que permite una búsqueda sistemática del espacio de unificadores (generalizar el algoritmo de unificación de Martelli -Montanari ^[2]con reglas para términos que contienen variables de orden superior) que parece funcionar suficientemente bien en la práctica. Huet ^[42] y Gilles Dowek ^[43] han escrito artículos sobre este tema.

Dale Miller ha descrito lo que ahora se llama unificación de patrones de orden superior . ^[44] Este subconjunto de unificación de orden superior es decidible y los problemas de unificación que se pueden resolver tienen unificadores más generales. Muchos sistemas informáticos que contienen unificación de orden superior, como los lenguajes de programación lógica de orden superior λProlog y Twelf , a menudo implementan solo el fragmento de patrón y no la unificación completa de orden superior.

En lingüística computacional, una de las teorías de elipsis más influyentes es que las elipses están representadas por variables libres cuyos valores se determinan luego mediante la unificación de orden superior (HOU). Por ejemplo, la representación semántica de "A Jon le gusta Mary y a Peter también" es como ( j , m ) ∧ R ( p ) y el valor de R (la representación semántica de la elipsis) está determinado por la ecuación como ( j , m ) = R ( j ) . El proceso de resolución de estas ecuaciones se llama unificación de orden superior. ^[45]

Por ejemplo, el problema de unificación { f ( a , b , a ) ≐ d ( b , a , c )}, donde la única variable es f , tiene las soluciones { 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 ( segundo , x , c )}, { f ↦ λ x .λ y .λ z . d ( b , z , c )} y { f ↦ λ x .λ y .λ z . d ( b, a , c )}.

Wayne Snyder dio una generalización tanto de la unificación de orden superior como de la unificación E, es decir, un algoritmo para unificar términos lambda módulo una teoría de ecuaciones. ^[46]

Ver también

• Reescritura
• Regla admisible
• Sustitución explícita en el cálculo lambda
• Resolución de ecuaciones matemáticas
• Desunificación : resolución de inecuaciones entre expresión simbólica
• Anti-unificación : calcular una generalización mínima general (lgg) de dos términos, dual para calcular una instancia más general (mgu)
• Alineación de ontología (use la unificación con equivalencia semántica )

Notas

1. en este caso, todavía existe un conjunto de sustitución completo (por ejemplo, el conjunto de todas las soluciones); sin embargo, cada uno de estos conjuntos contiene miembros redundantes.
2. Por ejemplo, a ⊕ ( b ⊕ f ( x )) ≡ a ⊕ ( f ( x ) ⊕ b ) ≡ ( b ⊕ f ( x )) ⊕ a ≡ ( f ( x ) ⊕ b ) ⊕ a
3. desde${\displaystyle (x\oplus y)\{x\mapsto z,y\mapsto z\}=z\oplus z\equiv z}$
4. ya que z { z ↦ x ⊕ y } = x ⊕ y
5. formalmente: cada unificador τ satisface ∀ x : xτ = ( xσ ) ρ para alguna sustitución ρ
6. Alg.1, p. 261. Su regla (a) corresponde a la regla de intercambio aquí, (b) a borrar , (c) a la vez se descomponen y el conflicto , y (d) a la vez eliminar y verificación .
7. Véase Martelli, Montanari (1982), ^[2] sección 1, p.259. El artículo de Paterson y Wegman está fechado en 1978; sin embargo, el editor de la revista lo recibió en septiembre de 1976.
8. Aunque la regla mantiene x ≐ t en G , no puederepetirseeternamente ya que su precondición x ∈ vars ( G ) es invalidada por su primera aplicación. De manera más general, se garantiza que el algoritmo terminará siempre, ver más abajo .
9. en presencia de igualdad C , las igualdades N _l y N _r son equivalentes, similares para D _l y D _r

Referencias

1. Fages, François; Huet, Gérard (1986). "Conjuntos completos de uniformes y igualadores en teorías de ecuaciones" . Informática Teórica . 43 : 189-200. doi : 10.1016 / 0304-3975 (86) 90175-1 .
2. Martelli, Alberto; Montanari, Ugo (abril de 1982). "Un algoritmo de unificación eficiente". ACM Trans. Programa. Lang. Syst . 4 (2): 258–282. doi : 10.1145 / 357162.357169 . S2CID 10921306 . 
3. J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie , Clase III, Sciences Mathématiques et Physiques, 33, 1930.
4. Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Conferencias sobre Jacques Herbrand como lógico (Informe SEKI). DFKI. arXiv : 0902.4682 . Aquí: p.56
5. Jacques Herbrand (1930). Recherches sur la théorie de la demostración (PDF) (tesis doctoral). A. 1252 . Université de Paris. Aquí: p.96-97
6. J.A. Robinson (enero de 1965). "Una lógica orientada a la máquina basada en el principio de resolución". Revista de la ACM . 12 (1): 23–41. doi : 10.1145 / 321250.321253 . S2CID 14389185 . ; Aquí: sección 5.8, p.32
7. JA Robinson (1971). "Lógica computacional: el cálculo de unificación" . Inteligencia de máquina . 6 : 63–72.
8. CC Chang ; H. Jerome Keisler (1977). Teoría de modelos . Estudios de Lógica y Fundamentos de las Matemáticas. 73 . Holanda Septentrional.; aquí: Sección 1.3
9. KR Apt. "De la programación lógica al prólogo", pág. 24. Prentice Hall, 1997.
10. Robinson (1965); ^[6] nr.2.5, 2.14, p.25
11. Robinson (1965); ^[6] nr ^. 5.6, p. 32
12. Robinson (1965); ^[6] nr.5.8, p.32
13. Lewis Denver Baxter (febrero de 1976). Un algoritmo de unificación prácticamente lineal (PDF) (Informe de resolución). CS-76-13. Univ. de Waterloo, Ontario.
14. Gérard Huet (septiembre de 1976). Resolution d'Equations dans des Langages d'Ordre 1,2, ... ω (These d'etat). Université de Paris VII.
15. Alberto Martelli y Ugo Montanari (julio de 1976). Unificación en tiempo y espacio lineales: una presentación estructurada (nota interna). IEI-B76-16. Consiglio Nazionale delle Ricerche, Pisa. Archivado desde el original el 15 de enero de 2015.
16. Michael Stewart Paterson y MN Wegman (abril de 1978). "Unificación lineal" . J. Comput. Syst. Sci . 16 (2): 158-167. doi : 10.1016 / 0022-0000 (78) 90043-0 .
17. JA Robinson (enero de 1976). "Unificación rápida" . En Woodrow W. Bledsoe , Michael M. Richter (ed.). Proc. Taller de demostración de teoremas Oberwolfach . Informe del taller de Oberwolfach. 1976/3.^{[ enlace muerto permanente ]}
18. M. Venturini-Zilli (octubre de 1975). "Complejidad del algoritmo de unificación para expresiones de primer orden". Calcolo . 12 (4): 361–372. doi : 10.1007 / BF02575754 . S2CID 189789152 . 
19. McBride, Conor (octubre de 2003). "Unificación de primer orden por recursividad estructural" . Revista de programación funcional . 13 (6): 1061–1076. CiteSeerX 10.1.1.25.1516 . doi : 10.1017 / S0956796803004957 . ISSN 0956-7968 . Consultado el 30 de marzo de 2012 .  
20. p. ej., Paterson, Wegman (1978), ^[16] sección 2, p.159
21. Walther, Christoph (1985). "Una solución mecánica de la apisonadora de Schubert por resolución variada" (PDF) . Artif. Intell . 26 (2): 217–224. doi : 10.1016 / 0004-3702 (85) 90029-3 . Archivado desde el original (PDF) en 2011-07-08 . Consultado el 28 de junio de 2013 .
22. Smolka, Gert (noviembre de 1988). Programación lógica con tipos ordenados polimórficamente (PDF) . En t. Taller de Programación Algebraica y Lógica. LNCS. 343 . Saltador. págs. 53–70. doi : 10.1007 / 3-540-50667-5_58 .
23. Schmidt-Schauß, Manfred (abril de 1988). Aspectos computacionales de una lógica ordenada por orden con declaraciones a plazo . LNAI. 395 . Saltador.
24. Gordon D. Plotkin , Propiedades teóricas de celosía de subsunción , Memorando MIP-R-77, Univ. Edimburgo, junio de 1970
25. Mark E. Stickel , Un algoritmo de unificación para funciones asociativas-conmutativas , J. Assoc. Computación. Mach., Vol. 28, n. ° 3, págs. 423–434, 1981
26. F. Fages, Unificación asociativa-conmutativa , J. Simbólica Comput., vol.3, no.3, pp. 257-275, 1987
27. Franz Baader, La unificación en semigrupos idempotentes es de tipo cero , J. Automat. Razonamiento, vol 2, no 3, 1986
28. J. Makanin, El problema de la solucion de ecuaciones en un semi-grupo libre , Akad. Nauk SSSR, vol. 233, n. ° 2, 1977
29. F. Fages (1987). "Unificación asociativa-conmutativa" (PDF) . J. Computación simbólica . 3 (3): 257–275. doi : 10.1016 / s0747-7171 (87) 80004-4 .
30. Martin, U., Nipkow, T. (1986). "Unificación en anillos booleanos". En Jörg H. Siekmann (ed.). Proc. 8º CADE . LNCS. 230 . Saltador. págs. 506–513.
31. A. Boudet; JP Jouannaud; M. Schmidt-Schauß (1989). "Unificación de anillos booleanos y grupos abelianos" . Revista de Computación Simbólica . 8 (5): 449–477. doi : 10.1016 / s0747-7171 (89) 80054-9 .
32. Baader y Snyder (2001), p. 486.
33. F. Baader y S. Ghilardi, Unificación en lógicas modales y descriptivas , Logic Journal of the IGPL 19 (2011), no. 6, págs. 705–730.
34. P. Szabo, Unifikationstheorie erster Ordnung ( Teoría de la unificación de primer orden ), Tesis, Univ. Karlsruhe, Alemania Occidental, 1982
35. Jörg H. Siekmann, Unificación universal , Proc. 7º Int. Conf. sobre la deducción automatizada, Springer LNCS vol.170, págs. 1-42, 1984
36. N. Dershowitz y G. Sivakumar, Resolución de objetivos en lenguajes equitativos, Proc. 1er Int. Taller sobre sistemas de reescritura de términos condicionales, Springer LNCS vol.308, págs. 45–55, 1988
37. Fay (1979). "Unificación de primer orden en una teoría ecuacional". Proc. 4º Taller de Deducción Automatizada . págs. 161-167.
38. Warren D. Goldfarb (1981). "La indecidibilidad del problema de unificación de segundo orden" . TCS . 13 (2): 225–230. doi : 10.1016 / 0304-3975 (81) 90040-2 .
39. Gérard P. Huet (1973). "La indecidibilidad de la unificación en la lógica de tercer orden" . Información y control . 22 (3): 257–267. doi : 10.1016 / S0019-9958 (73) 90301-X .
40. Claudio Lucchesi: La indecidibilidad del problema de unificación para lenguajes de tercer orden (Informe de investigación CSRR 2059; Departamento de Ciencias de la Computación, Universidad de Waterloo, 1972)
41. Gérard Huet: Un algoritmo de unificación para Lambda-Calculus tipado []
42. Gérard Huet: Unificación de orden superior 30 años después
43. Gilles Dowek: Unificación y emparejamiento de orden superior. Manual de razonamiento automatizado 2001: 1009–1062
44. Miller, Dale (1991). "Un lenguaje de programación lógica con abstracción Lambda, variables de función y unificación simple" (PDF) . Revista de Lógica y Computación . 1 (4): 497–536. doi : 10.1093 / logcom / 1.4.497 .
45. Gardent, Claire; Kohlhase, Michael ; Konrad, Karsten (1997). "Un enfoque de unificación de varios niveles, de orden superior para elipsis". Enviado a la Asociación Europea de Lingüística Computacional (EACL) . CiteSeerX 10.1.1.55.9018 . 
46. Wayne Snyder (julio de 1990). "E-unificación de orden superior". Proc. X Congreso de Deducción Automatizada . LNAI. 449 . Saltador. págs. 573–587.

Otras lecturas

• Franz Baader y Wayne Snyder (2001). "Teoría de la unificación" Archivado el 8 de junio de 2015 en la Wayback Machine . En John Alan Robinson y Andrei Voronkov , editores, Handbook of Automated Reasoning , volumen I, páginas 447–533. Editores de ciencia de Elsevier. ^{[ enlace muerto ]}
• Gilles Dowek (2001). "Unificación y emparejamiento de orden superior" . En Manual de razonamiento automatizado .
• Franz Baader y Tobias Nipkow (1998). Reescritura de términos y todo eso . Prensa de la Universidad de Cambridge.
• Franz Baader y Jörg H. Siekmann  [ de ] (1993). "Teoría de la unificación". En Manual de Lógica en Inteligencia Artificial y Programación Lógica .
• Jean-Pierre Jouannaud y Claude Kirchner (1991). "Resolver ecuaciones en álgebras abstractas: una encuesta de unificación basada en reglas". En Computational Logic: Ensayos en honor a Alan Robinson .
• Nachum Dershowitz y Jean-Pierre Jouannaud , Rewrite Systems , en: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science , volumen B Modelos formales y semántica , Elsevier, 1990, págs. 243–320
• Jörg H. Siekmann (1990). "Teoría de la unificación". En Claude Kirchner (editor) Unificación . Prensa académica.
• Kevin Knight (marzo de 1989). "Unificación: una encuesta multidisciplinaria" (PDF) . Encuestas de computación ACM . 21 (1): 93-124. CiteSeerX  10.1.1.64.8967 . doi : 10.1145 / 62029.62030 . S2CID  14619034 .
• Gérard Huet y Derek C. Oppen (1980). "Ecuaciones y reglas de reescritura: una encuesta" . Reporte técnico. Universidad Stanford.
• Raulefs, Peter; Siekmann, Jörg; Szabó, P .; Unvericht, E. (1979). "Una breve encuesta sobre el estado del arte en problemas de emparejamiento y unificación". Boletín ACM SIGSAM . 13 (2): 14-20. doi : 10.1145 / 1089208.1089210 . S2CID  17033087 .
• Claude Kirchner y Hélène Kirchner. Reescribir, resolver, probar . En la preparación de.