El proceso algorítmico de encontrar una sustitución (mapeo de variables a términos) que haga que dos expresiones simbólicas sean idénticas hasta igualdad sintáctica (o igualdad módulo una teoría); central en razonamiento automático, inferencia de tipos y programación lógica.

Principio

Buscar un unificador más general (mgu) que resuelva las ecuaciones de emparejamiento entre sub‑términos correspondientes sin introducir instanciaciones innecesarias; la comprobación de ocurrencia (occur‑check) evita sustituciones cíclicas, y las variantes incluyen unificación sintáctica de primer orden, E‑unificación (módulo teorías ecuacionales) y unificación de orden superior con perfiles de decidibilidad y complejidad muy distintos.

Demostración

Ejemplo de primer orden: unificar f(x,a) y f(b,y) — el mgu es {x↦b, y↦a}. Ejemplo de occur‑check: unificar x y f(x) falla porque cualquier solución sería cíclica (en unificación de primer orden el occur‑check rechaza esto). Ejemplo de orden superior: la unificación en el cálculo λ es indecidible en general y requiere algoritmos diferentes (p. ej. procedimientos semi‑decidibles de Huet) o restricciones para obtener decidibilidad.

Aplicación incorrecta

Omitir el occur‑check en implementaciones produce sustituciones no válidas que permiten términos infinitos y respuestas erróneas. Aplicar algoritmos de unificación de primer orden a problemas con operadores asociativos/ conmutativos o ligados de orden superior sin usar la maquinaria de E‑unificación o de orden superior apropiada conduce a una unificación incorrecta o incompleta.

Consecuencia

La unificación produce las sustituciones necesarias para la resolución en demostración de primer orden, para la inferencia de tipos en lenguajes de programación y para el emparejamiento en sistemas de reescritura; cuando existen mgus permiten soluciones generales y reutilizables, mientras que la intractabilidad o indecidibilidad en marcos más expresivos limita el razonamiento automático y requiere heurísticas o fragmentos restringidos.

Inversión

Matching (unificación unilateral) restringe las variables a una expresión y es computacionalmente más simple; la antiunificación (generalización) calcula los generalizadores menos generales en lugar de los unificadores más generales. Invertir la unificación desplaza conceptualmente de resolver ecuaciones a encontrar abstracciones esquemáticas.

Límite

La unificación sintáctica de primer orden es decidible y tiene unificadores más generales cuando es soluble; la unificación módulo teorías (AC, asociativo‑conmutativo, etc.) o la unificación de orden superior puede ser indecidible o de complejidad mucho mayor. Las propiedades exactas dependen de la lógica y la teoría en que se realiza la unificación.

Tensión semántica

Tensión entre la unificación sintáctica (estructura pura del término) y la unificación semántica (módulo teorías) afecta tanto la completitud como el rendimiento; aparecen compensaciones entre un razonamiento equacional más rico y la tratabilidad algorítmica.

Síntesis

La unificación es el proceso de calcular sustituciones que hacen iguales a los términos según una noción elegida de igualdad; como operación central en deducción automática y sistemas de tipos equilibra el deseo de soluciones más generales y reutilizables con las limitaciones impuestas por comprobaciones de ocurrencia, teorías ecuacionales y características de orden superior, que alteran la decidibilidad y la complejidad.