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. 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 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, pero la primera investigación formal puede ser atribuida a John Alan Robinson, 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\to$ ℙ$(V)$, asignando a cada término $t$ el conjunto $\text{vars}(t)⊊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. 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\ge 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:

• 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.

Sustitución

Sustitución es un mapeo $\sigma :V\to 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 Plantilla:Math} al término

	$f($	$\mathbf{\text{x}}$	$,a,g($	$\mathbf{\text{z}}$	$),y)$
resulta en
	$f($	$\mathbf{\text{h}}(\mathbf{\text{a}},\mathbf{\text{y}})$	$,a,g($	$\mathbf{\text{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$, y viceversa, 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)$.

Problema de unificación, conjunto de soluciones

Un problema de unificación es un conjunto finito Plantilla:Math} de ecuaciones potenciales, donde Plantilla:Math. Una sustitución σ es una solución de este problema si Plantilla:Math 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

Diagrama esquemático triangular de la unificación sintáctica de términos t₁ and t₂ mediante sustitución σ

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 Plantilla:Math} que tenga solución tiene un conjunto de soluciones unitario Plantilla:Math} que es completo y obviamente mínimo. El miembro Plantilla:Mvar es llamado unificador más general (mgu por sus siglas en inglés) 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 Plantilla:Math. Cualquier unificador del problema es subsumido por el mgu Plantilla:Mvar. 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 Plantilla:Math y Plantilla:Math y Plantilla:Math es una variante de Plantilla:Math 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

Plantilla:Quote box El primer algoritmo dado por Robinson (1965) era bastante ineficiente; cf. box. Luego hubo un algoritmo más eficiente originado en Martelli, Montanari (1982). Este documento también enlista otros intentos previos para encontrar un algoritmo de unificación sintáctica más eficiente, y afirma que los algoritmos de tiempo lineal fueron descubiertos independientemente por Martelli, Montanari (1976) y Paterson, Wegman (1978).Plantilla:Refn

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,\dots ,s_k)\doteq g(t_0,...,t_m)\}$	$\Rightarrow$	$\mathrm{\perp }$	if $f\ne g$ or $k\ne 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\in ̸\text{vars}(t)$ and $x\in \text{vars}(G)$	eliminar
$G\cup \{x\doteq f(s_0,...,s_k)\}$	$\Rightarrow$	$\mathrm{\perp }$	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 $⟨n_{var},n_{lhs},n_{eqn}⟩$ donde Plantilla:Math es el número de variables que ocurren más de una vez en el conjunto de ecuaciones, Plantilla:Math es el número de símbolos de función y constantes en el lado izquierdo de las ecuaciones potenciales, y Plantilla:Math es el número de ecuaciones. Cuando se aplica la regla eliminar, Plantilla:Math disminuye, ya que x se elimina de G y permanece solo en {x≐t}. La aplicación de cualquier otra regla nunca puede aumentar Plantilla:Math nuevamente. Cuando se aplica la regla descomponer, conflicto o intercambio, Plantilla:Math 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 Plantilla:Math, pero disminuye Plantilla:Math. Por lo tanto, cualquier aplicación de las reglas disminuye el triple $⟨n_{var},n_{lhs},n_{eqn}⟩$ con respecto al orden lexicográfico, que es posible solo un número finito de veces.

Conor McBride observa 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 Plantilla:Mvar puede tener un tamaño de Plantilla:Math. 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.Plantilla:Refn