El proceso de hallar sustituciones para variables que hacen que dos expresiones sintácticas (términos) sean idénticas según el álgebra de términos de una lógica; devuelve una sustitución que asigna variables a términos cuando existe solución.

Principio

Resolver un conjunto finito de ecuaciones de términos mediante la descomposición repetida de términos compuestos, la orientación de igualdades que involucran variables, la comprobación de ocurrencias para evitar sustituciones cíclicas y el cálculo del unificador más general cuando es posible.

Demostración

Unificar f(x, a) y f(b, y) produce la sustitución {x ↦ b, y ↦ a}. En resolución de primer orden, la unificación se usa para hacer literales sintácticamente iguales antes de aplicar la regla de resolución.

Aplicación incorrecta

Omitir la comprobación de ocurrencia y aceptar sustituciones como x ↦ f(x) genera términos cíclicos o mal fundados; o asumir que la unificación siempre produce una sustitución única, cuando en contextos teóricos o de orden superior pueden existir varios unificadores no comparables o ninguno.

Consecuencia

Aplicada correctamente, la unificación proporciona las sustituciones necesarias para demostración automática, programación lógica e inferencia de tipos; el unificador más general conserva la máxima generalidad, facilitando la reutilización y composición de pruebas o programas.

Inversión

La noción inversa es la antiunificación (generalización), que busca la generalización menos específica de dos términos en lugar de una sustitución que los haga iguales; conceptualmente, la inversión cambia de resolver ecuaciones a encontrar estructura común.

Límite

La unificación estándar (de primer orden) asume un álgebra sintáctica de términos sin teorías incorporadas; excluye la unificación ecuacional o módulo teoría (p. ej. módulo asociatividad o conmutatividad) y la unificación de orden superior, salvo que se indique lo contrario, cada una con algoritmos y propiedades de decidibilidad distintas.

Tensión semántica

Hay tensión entre unificación y pattern matching: el matching fija un lado como patrón a instanciar, produciendo sustituciones unidireccionales especializadas, mientras que la unificación es simétrica y puede devolver sustituciones más generales; otra tensión es entre unificación sintáctica y unificación sensible a teorías.

Síntesis

La unificación es un solucionador algorítmico de ecuaciones sintácticas de términos: descomponiendo estructuras, aplicando restricciones de ocurrencia y calculando unificadores más generales, suministra las sustituciones que permiten la instanciación de variables en inferencia, programación y verificación de tipos.