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 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. 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,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. Here: p.56 Here: p.96-97 pero la primera investigación formal puede ser atribuida a John Alan Robinson,; Here: sect.5.8, p.32 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 de variables. Para unificación de orden superior es conveniente escoger un diferente de un conjunto de variables ligadas en expresiones lambda. Un conjunto de términos tales que . Para unificaciones de primer orden y unificaciones de orden superior, 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: ℙ, asignando a cada término el conjunto de variables libres en . Una relación de equivalencia on , indicando que términos son considerados iguales. En unificación de orden superior, usualmente si y son alpha equivalentes. En E-Unificación de primer orden, refleja el conocimiento previo sobre ciertas funciones; por ejemplo, si es considerado conmutativo, si es el resultado de intercambiando los argumentos de con algunas (posiblemente todas) las ocurrencias.E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a 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 de variables, un conjunto de constantes y varios conjuntos de n funciones, también llamados operadores, por cada número natural , el conjunto de términos (de primero orden sin clasificar) se define recursivamente como el conjunto más pequeño con las siguientes propiedades:; here: Sect.1.3 Cada variable es un término: , Cada constante es un término: , A partir de cada n términos , y cada n función , se puede crear un término más grande . Por ejemplo, si es una variable, es una constante, y es una función binaria, entonces , y (por lo tanto) por la primera, segunda y tercera regla de construcción de términos respectivamente. El último término se escribe usualmente como , 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

Sustitución Sustitución es un mapeo desde variables hacia terms; la notación se refiere a una sustitución mapeando cada variable con el término , para , y cada otra variable consigo misma. Aplicar esa sustitución a un término se escribe utilizando notación de posfijo: ; que significa reemplazar (simultáneamente) cada ocurrencia la variable en el término con . El resultado de haber aplicado una sustitución a un término se llama una instancia de ese término . Un ejemplo de primer orden, aplicando la sustitución } al término resulta en  

Generalización, especialización

Si un término tiene una instancia equivalente a un término , esto es, si por alguna sustitución , entonces se dice que es más general que , y que es más especial que, o subsumido por, . Por ejemplo, es más general que si ⊕ es conmutativa, considerando que .

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,

es una variante de , dado que

y .

Sin embargo, no es una variante de , 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 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 , entonces el término es más general que ,Considerando que y viceversa,Dado que a pesar de que y tienen una estructura diferente.

Una sustitución es más especial que, o subsumida por, una sustitución si is más especial que para cada término . Se dice también que es más general que . Por ejemplo es más especial que , pero no lo es, porque no es más especial que .K.R. Apt. "From Logic Programming to Prolog", p. 24. Prentice Hall, 1997.

Problema de unificación, conjunto de soluciones

Un problema de unificación es un conjunto finito } de ecuaciones potenciales, donde . Una sustitución σ es una solución de este problema si para . 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 Fn de n funciones) y en que ≡ es una igualdad sintáctica. En este esquema, cada problema de unificació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ésEn el texto se utilizarán las 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 . Cualquier unificador del problema es subsumidoFormalmente: cada unificador τ satisface por alguna sustitución ρ por el mgu . El mgu es único: si S 1 y S 2 son conjuntos de soluciones completos y mínimos del mismo problema de unificación sintáctica, entonces S 1 = { σ 1 } y S 2 = { σ 2 } para algunas sustituciones y y es una variante de 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

| align="right" | x | { x ↦ z, y ↦ f(z) }

| align="center" | z

| align="right" | z | { x ↦ z, y ↦ f(z) } |, y |- | align="right" | y | { x ↦ z, y ↦ f(z) }

| align="center" | f(z)

| align="right" | 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(x1), y ↦ f(f(x1)), z ↦ f(x1) }, { x ↦ f(f(x1)), y ↦ f(f(f(x1))), z ↦ f(f(x1)) }, 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