Unificación (ciencias de la computación)

En lógica y en ciencias de la computación, la unificación es un proceso algorítmico para resolución de ecuaciones con expresiones simbólicas.

Se pueden determinar diferentes esquemas de unificación dependiendo de: qué expresiones (también llamadas términos) están permitidas en un conjunto de ecuaciones (también llamado problema de unificación), y de cuáles expresiones son consideradas homólogas. Si variables de orden superior, esto es, variables que representan funciones, son permitidas en una expresión, el proceso es llamado unificación de orden superior, si no se llama unificación de primer orden. Si una solución requiere hacer ambos lados de cada ecuación literalmente iguales entonces el proceso se llama sintáctico o unificación libre, de lo contrario semántico o unificación ecuacional, o E-Unificación o teoría de unificación modular.

Una solución de un problema de unificación se denota como una sustitución, esto es, un mapeo asignando un valor simbólico a cada una de las variables en las expresiones del problema. Un algoritmo de unificación debe calcular un conjunto de sustituciones completo y mínimo para un problema dado; esto es, un conjunto que cubra todas las soluciones y que no contenga miembros redundantes. De acuerdo con el marco de referencia, un conjunto de sustituciones completo y mínimo puede que tenga a lo más un miembro, a lo sumo una cantidad finita, o posiblemente infinito número de miembros, o no tener ninguno del todo.^{[note 1]}^[1] En algunos marcos de referencia es generalmente imposible decidir siquiera si existe alguna solución. Para unificaciones sintácticas de primer orden, Martelli y Montanari^[2] brindaron un algoritmo que reporta insolubilidd o calcula un conjunto completo y mínimo de sustituciones unitario que contiene el así llamado unificador más general.

Por ejemplo, usando x,y,z como variables, el conjunto de ecuaciones unitario { cons(x,cons(x,nil)) = cons(2,y) } es un problema de unificación sintáctico de primer orden que tiene la sustitución { x ↦ 2, y ↦ cons(2,nil) } como única solución. El problema de unificación sintáctico de primer orden { y = cons(2,y) } no tiene solución en el conjunto finite terms; sin embargo, tiene una solución única { y ↦ cons(2,cons(2,cons(2,...))) } en el conjunto de árboles infinitos. El problema de unificación semántica de primer orden { a⋅x = x⋅a } tiene cualquier sustitución de la forma { x ↦ a⋅...⋅a } como solución en un semigrupo, en otras palabras, si (⋅) es asociativa; el mismo problema, visto en un grupo abeliano donde (⋅) también es considerada conmutativa, tiene cualquier sustitución como una solución. El conjunto unitario { a = y(x) } es un problema de unificación sintáctico de segundo orden dado que y es una variable que representa una función. Una solución es { x ↦ a, y ↦ (función identidad) }; otra solución es { y ↦ (función constante asociando cada valor con a), x ↦ (cualquier valor) }.

Los algoritmos de unificación fueron descubiertos por Jacques Herbrand,^[3]^[4]^[5] pero la primera investigación formal puede ser atribuida a John Alan Robinson,^[6]^[7] quien utilizó unificación sintáctica de primer orden como base en su procedimiento de resolución de lógica de primer orden, un gran paso adelante en la tecnología de razonamiento automatizado al eliminar una de las fuentes de explosión combinatoria: la búsqueda de instanciación de términos. El razonamiento automático es todavía el área donde la unificación es aplicada mayormente. Unificación sintáctica de primer orden es usada en programación lógica y en la implementación de lenguajes de programación que usan tipos, especialmente en algoritmos de inferencia de tipos basados en Hindley–Milner. Unificación semántica es utilizada en solucionadores de satisfacibilidad módulo (SMT por las siglas en inglés), algoritmos para la conversión de términos (reescritura de términos) y en análisis de protocolos criptográficos. Unificación de orden superior es utilizado en asistentes para la demostración de teoremas, por ejemplo Isabelle and Twelf, y formas restringidas de unificación de orden superior (unificación de patrones de nivel orden superior) son utilizadas en la implementación de algunos lenguajes de programación, tales como lambdaProlog, porque pese a que los patrones de orden superior son expresivos, 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 $V$ de variables. Para unificación de orden superior es conveniente escoger un $V$ diferente de un conjunto de variables ligadas en expresiones lambda.
Un conjunto $T$ de términos tales que $V\subseteq T$ . Para unificaciones de primer orden y unificaciones de orden superior, $T$ es usualmente el conjunto de términos de primer orden (términos construidos con variables y funciones) para el primero y términos Lambda (términos con algunas variables de orden superior) para el segundo.
Un mapeo vars: $T\rightarrow$ ℙ $(V)$ , asignando a cada término $t$ el conjunto ${\text{vars}}(t)\subsetneq V$ de variables libres en $t$ .
Una relación de equivalencia $\equiv$ on $T$ , indicando que términos son considerados iguales. En unificación de orden superior, usualmente $t\equiv u$ si $t$ y $u$ son alpha equivalentes. En E-Unificación de primer orden, $\equiv$ refleja el conocimiento previo sobre ciertas funciones; por ejemplo, si $\oplus$ es considerado conmutativo, $t\equiv u$ si $u$ es el resultado de $t$ intercambiando los argumentos de $\oplus$ con algunas (posiblemente todas) las ocurrencias.^{[note 2]} Si no hay conocimiento previo del todo, entonces solo términos literalmente, o sintácticamente, idénticos son considerados iguales; en este caso, ≡ es llamado teoría libre (porque es un objeto libre), teoría vacía (porque el conjunto de sentencias, o el conocimiento previo, está vacío), o teoría de constructores (porque todas las funciones solo crean términos de datos, en lugar de operaciones en ellos).

Término de primer orden

Dado un conjunto $V$ de variables, un conjunto $C$ de constantes y varios conjuntos $F_{n}$ de n funciones, también llamados operadores, por cada número natural $n\geq 1$ , el conjunto de términos (de primero orden sin clasificar) $T$ se define recursivamente como el conjunto más pequeño con las siguientes propiedades:^[8]

Cada variable es un término: $V\subseteq T$ ,
Cada constante es un término: $C\subseteq T$ ,
A partir de cada n términos $t_{1},...t_{n}$ , y cada n función $f\in F_{n}$ , se puede crear un término más grande $f(t_{1},...,t_{n})$ .

Por ejemplo, si $x\in V$ es una variable, $1\in C$ es una constante, y ${\text{add}}\in F_{2}$ es una función binaria, entonces $x\in T,1\in T$ , y (por lo tanto) ${\text{add}}(x,1)\in T$ por la primera, segunda y tercera regla de construcción de términos respectivamente. El último término se escribe usualmente como $x+1$ , usando notación using notación de infijo y por conveniencia se utiliza el símbolo + que es un operador más común.

Términos de orden superior

Artículo principal: Cálculo lambda

Sustitución

Sustitución es un mapeo $\sigma :V\rightarrow T$ desde variables hacia terms; la notación $\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$ se refiere a una sustitución mapeando cada variable $x_{i}$ con el término $t_{i}$ , para $i=1,...,k$ , y cada otra variable consigo misma. Aplicar esa sustitución a un término $t$ se escribe utilizando notación de posfijo: $t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$ ; que significa reemplazar (simultáneamente) cada ocurrencia la variable $x_{i}$ en el término $t$ con $t_{i}$ . El resultado $t\tau$ de haber aplicado una sustitución $\tau$ a un término $t$ se llama una instancia de ese término $t$ . Un ejemplo de primer orden, aplicando la sustitución ${x \mapsto h (a, y), z \mapsto b$ } al término

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

Generalización, especialización

Si un término $t$ tiene una instancia equivalente a un término $u$ , esto es, si $t\sigma \equiv u$ por alguna sustitución $\sigma$ , entonces se dice que $t$ es más general que $u$ , y que $u$ es más especial que, o subsumido por, $t$ . Por ejemplo, $x\oplus a$ es más general que $a\oplus b$ si ⊕ es conmutativa, considerando que $(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 o más especial que otro solo si ambos términos difieren solo en sus nombres de variable, no en su estructura sintáctica; tales términos se denominan variantes o renombramientos entre sí. Por ejemplo,

$f(x_{1},a,g(z_{1}),y_{1})$ es una variante de $f(x_{2},a,g(z_{2}),y_{2})$ , dado que

$f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})$

y

$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, $f(x_{1},a,g(z_{1}),y_{1})$ no es una variante de $f(x_{2},a,g(x_{2}),x_{2})$ , dado que no existe una sustitución que devuelva el primer término a partir del segundo. El último término es, por consiguiente, más especial que el primer término.

Para una $\equiv$ arbitraria, un término puede ser más general o más específico que un término estructuralmente diferente. Por ejemplo, si ⊕ es idempotente, esto es, si siempre $x\oplus x\equiv x$ , entonces el término $x\oplus y$ es más general que $z$ ,^{[note 3]} y viceversa,^{[note 4]} a pesar de que $x\oplus y$ y $z$ tienen una estructura diferente.

Una sustitución $\sigma$ es más especial que, o subsumida por, una sustitución $\tau$ si $t\sigma$ is más especial que $t\tau$ para cada término $t$ . Se dice también que $\tau$ es más general que $\sigma$ . Por ejemplo $\{x\mapsto a,y\mapsto a\}$ es más especial que $\tau =\{x\mapsto y\}$ , pero $\sigma =\{x\mapsto a\}$ no lo es, porque $f(x,y)\sigma =f(a,y)$ no es más especial que $f(x,y)\tau =f(y,y)$ .^[9]

Problema de unificación, conjunto de soluciones

Un problema de unificación es un conjunto finito ${l 1 ≐ r 1, ..., l n ≐ r n$ } de ecuaciones potenciales, donde $l i, r i \in T$ . Una sustitución σ es una solución de este problema si $l i σ \equiv r i σ$ para $i=1,...,n$ . Tal sustitución se llama también un unificador del problema de unificación. Por ejemplo, if ⊕ is asociativa, el problema de unificación { x ⊕ a ≐ 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, se dice que un conjunto S de unificadores es completo si cada solución es subsumida por alguna sustitución σ ∈ S; el conjunto S es llamado mínimo si ninguno de sus miembros subsume algún otro.

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

Unificación sintáctica de términos de primer orden es el esquema de unificación más utilizado. Está basado en T siendo este un conjunto de términos de primer orden (sobre un conjunto dado V de variables, C de constantes y F_n de n funciones) y en que ≡ es una igualdad sintáctica. En este esquema, cada problema de unificación ${l 1 ≐ r 1, ..., l n ≐ r n$ } que tenga solución tiene un conjunto de soluciones unitario ${σ$ } que es completo y obviamente mínimo. El miembro $σ$ es llamado unificador más general (mgu por sus siglas en inglés^{[NT 1]}) del problema. Los términos izquierdo y derecho de cada ecuación potencial se vuelven sintácticamente iguales cuando se aplica el mgu, por ejemplo $l 1 σ = r 1 σ \land ... \land l n σ = r n σ$ . Cualquier unificador del problema es subsumido^{[note 5]} por el mgu $σ$ . El mgu es único: si S ₁ y S ₂ son conjuntos de soluciones completos y mínimos del mismo problema de unificación sintáctica, entonces S ₁ = { σ ₁} y S ₂ = { σ ₂} para algunas sustituciones $σ 1$ y $σ 2,$ y $xσ 1$ es una variante de $xσ 2$ para cada variable x que ocurra 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 { x ↦ f(x₁), y ↦ f(f(x₁)), z ↦ f(x₁) }, { x ↦ f(f(x₁)), y ↦ f(f(f(x₁))), z ↦ f(f(x₁)) }, y así sucesivamente; hay una cantidad infinita de unificadores similares.

Otro ejemplo, el problema g(x,x) ≐ f(y) no tiene solución con respecto a ≡ como identidad literal, ya que cualquier sustitución aplicada al lado izquierdo y derecho mantendrá la g y la 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 Robinson (1965)

Los símbolos se ordenan tal que las variables preceden a las funciones. Los términos se ordenan de acuerdo con su extensión y términos de igual tamaño se ordenan lexicográficamente.^[10] Para un conjunto T de términos, la ruta de desacuerdo p es la ruta lexicográficamente mínima donde dos términos miembros de T difieren. Su conjunto de desacuerdos es el conjunto de subtérminos que inician en p, formalmente: $t\in T$ }.^[11]

Algoritmo:^[12]

Dado un conjunto T de términos para ser unificados
Sea  $\sigma$  inicialmente la sustitución identidad.

hacer para siempre
  si  $T\sigma$  es un conjunto unitario entonces
    devuelva  $\sigma$ 
  fin-si 
  
  sea D el conjunto de desacuerdos de  $T\sigma$ 
  sea s, t los dos términos lexicográficamente menores en D
  
  si s no es una variable o s está en t entonces
    devuelva "NOUNIFICABLE"
  fin-si 
   $\sigma :=\sigma \{s\mapsto t\}$ 
final

El primer algoritmo dado por Robinson (1965) era bastante ineficiente; cf. box. Luego hubo un algoritmo más eficiente originado en Martelli, Montanari (1982).^{[note 6]} Este documento también enlista otros intentos previos para encontrar un algoritmo de unificación sintáctica más eficiente,^[13]^[14]^[15]^[16]^[17]^[18] y afirma que los algoritmos de tiempo lineal fueron descubiertos independientemente por Martelli, Montanari (1976)^[15] y Paterson, Wegman (1978).^[16]^{[note 7]}

Dado un conjunto finito $G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}$ de ecuaciones potenciales, el algoritmo aplica reglas para transformarlo en un conjunto de ecuaciones equivalentes, de la forma { x₁ ≐ u₁, ..., x_m ≐ u_m } donde x₁, ..., x_m son variables diferentes y u₁, ..., u_m son términos que no contienen a ninguna de las x_i. Un conjunto de esta forma puede ser una sustitución. Si no hay solución el algoritmo termina con ⊥; otros autores usan "Ω", "{}", o "fallo". La acción de sustituir todas las ocurrencias de x en un problema G con el término t se denota G {x ↦ t}. Por simplicidad, las constantes se Para simplificar, los símbolos constantes se consideran símbolos de función que tienen cero argumentos.

$G\cup \{t\doteq t\}$	$\Rightarrow$	$G$		borrar
$G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}$	$\Rightarrow$	$G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}$		descomponer
$G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}$	$\Rightarrow$	$\bot$	if $f\neq g$ or $k\neq m$	conflicto
$G\cup \{f(s_{0},...,s_{k})\doteq x\}$	$\Rightarrow$	$G\cup \{x\doteq f(s_{0},...,s_{k})\}$		intercambio
$G\cup \{x\doteq t\}$	$\Rightarrow$	$G\{x\mapsto t\}\cup \{x\doteq t\}$	if $x\not \in {\text{vars}}(t)$ and $x\in {\text{vars}}(G)$	eliminar^{[note 8]}
$G\cup \{x\doteq f(s_{0},...,s_{k})\}$	$\Rightarrow$	$\bot$	if $x\in {\text{vars}}(f(s_{0},...,s_{k}))$	check

Revisión de ocurrencia

El intento de unificar una variable x con un término que contenga x como un subtérmino estricto x ≐ f(..., x, ...) podría generar un término infinito como solución de para x, dado que x puede aparecer como un subtérmino de sí mismo. La ecuación x ≐ f(..., x, ...) no tiene solución en el conjunto finito de términos de primer orden definido arriba; puesto que la regla de eliminación solo puede ser aplicada si x ∉ vars(t). La revisión de ocurrencia es omitida en la mayoría de los sistemas Prolog porque hace que el algoritmo se vuelva lento.

Prueba de finalización

Para la prueba de finalización del algoritmo, considere un triple $\langle n_{var},n_{lhs},n_{eqn}\rangle$ 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 permanece solo en {x≐t}. La aplicación de cualquier otra regla nunca puede aumentar $n var$ nuevamente. Cuando se aplica la regla descomponer, conflicto o intercambio, $n lhs$ disminuye, ya que por lo menos desaparece la "f" más externa del lado izquierdo. La aplicación de cualquiera de las reglas restantes eliminar o revisar no puede aumentar $n lhs$ , pero disminuye $n eqn$ . Por lo tanto, cualquier aplicación de las reglas disminuye el triple $\langle n_{var},n_{lhs},n_{eqn}\rangle$ con respecto al orden lexicográfico, que es posible solo un número finito de veces.

Conor McBride observa^[19] que "expresando la estructura que explota la unificación" en un lenguaje tipo dependiente como Epigram, el algoritmo de John Alan Robinson se puede hacer recursivo en el número de variables, en cuyo caso una prueba de finalizació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 "and". 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 Prolog	Notación Matemática	Sustitución	Explicación
`a = a`	{ a = a }	{}	Exitoso. (tautología)
`a = b`	{ a = b }	⊥	a y b no coinciden
`X = X`	{ x = x }	{}	Exitoso. (tautología)
`a = X`	{ a = x }	{ x ↦ a }	x es unificada con la constante a
`X = Y`	{ x = y }	{ x ↦ y }	x e y son seudónimos
`f(a,X) = f(a,b)`	{ f(a,x) = f(a,b) }	{ x ↦ b }	símbolos de función y de constante coinciden, x es unificada con la constante a
`f(a) = g(a)`	{ f(a) = g(a) }	⊥	f y g no coinciden
`f(X) = f(Y)`	{ f(x) = f(y) }	{ x ↦ y }	x e y son seudónimos
`f(X) = g(Y)`	{ f(x) = g(y) }	⊥	f y g no coinciden
`f(X) = f(Y,Z)`	{ f(x) = f(y,z) }	⊥	Fallo. Los símbolos de función f tienen diferente cantidad de argumentos
`f(g(X)) = f(Y)`	{ f(g(x)) = f(y) }	{ y ↦ g(x) }	Unifica y con el término $g(x)$
`f(g(X),X) = f(Y,a)`	{ f(g(x),x) = f(y,a) }	{ x ↦ a, y ↦ g(a) }	Unifica x con la constante a, y y con el término $g(a)$
`X = f(X)`	{ x = f(x) }	debe ser ⊥	Retorna ⊥ en lógica de primer orden y en varios dialectos modernos de Prolog (enforzado por la revisión de ocurrencia). Exitoso en Prolog tradicional y en Prolog II, unificación de x con un término infinito `x=f(f(f(f(...))))`.
`X = Y, Y = a`	{ x = y, y = a }	{ x ↦ a, y ↦ a }	Ambos x y y son unificados con la constante a
`a = Y, X = Y`	{ a = y, x = y }	{ x ↦ a, y ↦ a }	Tal como se muestra arriba (no importa el orden de las ecuaciones en el conjunto)
`X = a, b = X`	{ x = a, b = x }	⊥	Falla. a y b no coinciden, por lo tanto x no se puede unificar con ninguno de los dos

Dos términos con un árbol exponencialmente más grande para su instancia menos común. Su representación gda (dag en inglés) es de tamaño linear (parte naranja a la derecha).

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 n$ . Por ejemplo, el problema $(((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))$ tiene el unificador más general $z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))$ , cf. imagen. Para evitar la complejidad de tiempo exponencial causada por tal explosión, los algoritmos de unificación avanzados trabajan con Grafo acíclico dirigido s (gad) en lugar de árboles.^[20]

Notas

↑ en este caso, todavía existe un conjunto completo de sustituciones (por ejemplo: el conjunto de todas las soluciones); sin embargo, cada una de estas soluciones contiene miembros redundantes.
↑ E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a
↑ Considerando que $(x\oplus y)\{x\mapsto z,y\mapsto z\}=z\oplus z\equiv z$
↑ Dado que $z {z \mapsto x \oplus y} = x \oplus y$
↑ Formalmente: cada unificador τ satisface $\forall x : xτ = (xσ) ρ$ por alguna sustitución ρ
↑ Alg.1, p.261. Su regla (a) corresponde con la regla intercambiar, (b) con borrar, (c) con descomponer y conflicto, y (d) con eliminar y revisar.
↑ See Martelli, Montanari (1982),^[2] sect.1, p.259. El documento de Paterson y Wegman está fechado en 1978, pero el editor de la revista lo recibió en septiembre 1976.
↑ Aunque la regla mantiene x ≐ t en G, no puede repetirse para siempre ya que la precondición x∈vars(G) se invalida en la primara aplicación. En forma más general, se garantiza que el algoritmo siempre finalice, véase más abajo.

Notas de traducción

↑ En el texto se utilizarán las siglas en inglés

Referencias

↑ Fages, François; Huet, Gérard (1986). «Complete Sets of Unifiers and Matchers in Equational Theories». Theoretical Computer Science 43: 189-200. doi:10.1016/0304-3975(86)90175-1.
↑ ^a ^b Martelli, Alberto; Montanari, Ugo (Apr 1982). «An Efficient Unification Algorithm». ACM Trans. Program. Lang. Syst. 4 (2): 258-282. doi:10.1145/357162.357169.
↑ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.
↑ Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009), Lectures on Jacques Herbrand as a Logician (SEKI Report) (SR-2009-01), DFKI, arXiv:0902.4682 . Here: p.56
↑ Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (Ph.D. thesis). A 1252. Université de Paris. Here: p.96-97
↑ ^a ^b ^c ^d J.A. Robinson (Jan 1965). «A Machine-Oriented Logic Based on the Resolution Principle». Journal of the ACM 12 (1): 23-41. doi:10.1145/321250.321253. ; Here: sect.5.8, p.32
↑ J.A. Robinson (1971). «Computational logic: The unification computation». Machine Intelligence 6: 63-72.
↑ C.C. Chang; H. Jerome Keisler (1977). Model Theory. Studies in Logic and the Foundation of Mathematics 73. North Holland. ; here: Sect.1.3
↑ K.R. Apt. "From Logic Programming to Prolog", p. 24. Prentice Hall, 1997.
↑ Robinson (1965);^[6] nr.2.5, 2.14, p.25
↑ Robinson (1965);^[6] nr.5.6, p.32
↑ Robinson (1965);^[6] nr.5.8, p.32
↑ Lewis Denver Baxter (Feb 1976), A practically linear unification algorithm (Res. Report), CS-76-13, Univ. of Waterloo, Ontario .
↑ Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (These d'etat). Universite de Paris VII.
↑ ^a ^b Alberto Martelli & Ugo Montanari (Jul 1976), Unification in linear time and space: A structured presentation (Internal Note), IEI-B76-16, Consiglio Nazionale delle Ricerche, Pisa, archivado desde el original el 15 de enero de 2015, consultado el 15 de octubre de 2020 .
↑ ^a ^b ^c Michael Stewart Paterson and M.N. Wegman (Apr 1978). «Linear unification». J. Comput. Syst. Sci. 16 (2): 158-167. doi:10.1016/0022-0000(78)90043-0.
↑ J.A. Robinson (Jan 1976). «Fast unification». En Woodrow W. Bledsoe, Michael M. Richter, ed. Proc. Theorem Proving Workshop Oberwolfach. Oberwolfach Workshop Report. 1976/3.
↑ M. Venturini-Zilli (Oct 1975). «Complexity of the unification algorithm for first-order expressions». Calcolo 12 (4): 361-372. S2CID 189789152. doi:10.1007/BF02575754.
↑ McBride, Conor (October 2003). «First-Order Unification by Structural Recursion». Journal of Functional Programming 13 (6): 1061-1076. ISSN 0956-7968. doi:10.1017/S0956796803004957. Consultado el 30 de marzo de 2012. Parámetro desconocido |citeseerx= ignorado (ayuda)
↑ e.g. Paterson, Wegman (1978),^[16] sect.2, p.159

Datos: Q609057
Multimedia: Unification (computer science) / Q609057

[1] ste caso, todavía existe un conjunto completo de sustituciones (por ejemplo: el conjunto de todas las soluciones); sin embargo, cada una de estas soluciones contiene miembros redundantes.

[9] E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a

[11] Considerando que $(x\oplus y)\{x\mapsto z,y\mapsto z\}=z\oplus z\equiv z$

[12] Dado que $z {z \mapsto x \oplus y} = x \oplus y$

[15] Formalmente: cada unificador τ satisface $\forall x : xτ = (xσ) ρ$ por alguna sustitución ρ

[19] Alg.1, p.261. Su regla (a) corresponde con la regla intercambiar, (b) con borrar, (c) con descomponer y conflicto, y (d) con eliminar y revisar.

[26] See Martelli, Montanari (1982),^[2] sect.1, p.259. El documento de Paterson y Wegman está fechado en 1978, pero el editor de la revista lo recibió en septiembre 1976.

[27] Aunque la regla mantiene x ≐ t en G, no puede repetirse para siempre ya que la precondición x∈vars(G) se invalida en la primara aplicación. En forma más general, se garantiza que el algoritmo siempre finalice, véase más abajo.

[14] En el texto se utilizarán las siglas en inglés

[2] Fages, François; Huet, Gérard (1986). «Complete Sets of Unifiers and Matchers in Equational Theories». Theoretical Computer Science 43: 189-200. doi:10.1016/0304-3975(86)90175-1.

[Martelli.Montanari.1982-3] Martelli, Alberto; Montanari, Ugo (Apr 1982). «An Efficient Unification Algorithm». ACM Trans. Program. Lang. Syst. 4 (2): 258-282. doi:10.1145/357162.357169.

[4] J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.

[5] Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009), Lectures on Jacques Herbrand as a Logician (SEKI Report) (SR-2009-01), DFKI, arXiv:0902.4682 . Here: p.56

[6] Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (Ph.D. thesis). A 1252. Université de Paris. Here: p.96-97

[Robinson.1965-7] J.A. Robinson (Jan 1965). «A Machine-Oriented Logic Based on the Resolution Principle». Journal of the ACM 12 (1): 23-41. doi:10.1145/321250.321253. ; Here: sect.5.8, p.32

[8] J.A. Robinson (1971). «Computational logic: The unification computation». Machine Intelligence 6: 63-72.

[10] C.C. Chang; H. Jerome Keisler (1977). Model Theory. Studies in Logic and the Foundation of Mathematics 73. North Holland. ; here: Sect.1.3

[13] K.R. Apt. "From Logic Programming to Prolog", p. 24. Prentice Hall, 1997.

[16] Robinson (1965);^[6] nr.2.5, 2.14, p.25

[17] Robinson (1965);^[6] nr.5.6, p.32

[18] Robinson (1965);^[6] nr.5.8, p.32

[20] Lewis Denver Baxter (Feb 1976), A practically linear unification algorithm (Res. Report), CS-76-13, Univ. of Waterloo, Ontario .

[21] Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (These d'etat). Universite de Paris VII.

[Martelli.Montanari.1976-22] Alberto Martelli & Ugo Montanari (Jul 1976), Unification in linear time and space: A structured presentation (Internal Note), IEI-B76-16, Consiglio Nazionale delle Ricerche, Pisa, archivado desde el original el 15 de enero de 2015, consultado el 15 de octubre de 2020 .

[Paterson.Wegman.1978-23] Michael Stewart Paterson and M.N. Wegman (Apr 1978). «Linear unification». J. Comput. Syst. Sci. 16 (2): 158-167. doi:10.1016/0022-0000(78)90043-0.

[24] J.A. Robinson (Jan 1976). «Fast unification». En Woodrow W. Bledsoe, Michael M. Richter, ed. Proc. Theorem Proving Workshop Oberwolfach. Oberwolfach Workshop Report. 1976/3.

[25] M. Venturini-Zilli (Oct 1975). «Complexity of the unification algorithm for first-order expressions». Calcolo 12 (4): 361-372. S2CID 189789152. doi:10.1007/BF02575754.

[28] McBride, Conor (October 2003). «First-Order Unification by Structural Recursion». Journal of Functional Programming 13 (6): 1061-1076. ISSN 0956-7968. doi:10.1017/S0956796803004957. Consultado el 30 de marzo de 2012. Parámetro desconocido |citeseerx= ignorado (ayuda)

[29] .g. Paterson, Wegman (1978),^[16] sect.2, p.159

[note 1]

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[note 2]

[8]

[note 3]

[note 4]

[9]

[NT 1]

[note 5]

[10]

[11]

[12]

[note 6]

[13]

[14]

[15]

[16]

[17]

[18]

[note 7]

[note 8]

[19]

[20]