unificació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 , 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 { (x,cons(x,)) = 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 ; sin embargo, tiene una solución única { y ↦ cons(2,cons(2,cons(2,...))) } en el conjunto de . 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 ,​​ 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 , especialmente en algoritmos de inferencia de tipos basados en . Unificación semántica es utilizada en solucionadores de satisfacibilidad módulo (SMT por las siglas en inglés), algoritmos para la (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 , 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 , 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.