Ver el código de «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 [[Fórmula (expresión)|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 [[Función matemática|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 (Lógica)|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.<ref group=note> 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.</ref><ref>{{cite journal|first1=François|last1=Fages|first2=Gérard|last2=Huet|title=Complete Sets of Unifiers and Matchers in Equational Theories|journal=Theoretical Computer Science|volume=43|pages=189–200|year=1986|doi=10.1016/0304-3975(86)90175-1}}</ref> 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<ref name="Martelli.Montanari.1982">{{cite journal|first1=Alberto|last1=Martelli|first2=Ugo|last2=Montanari|title=An Efficient Unification Algorithm|journal=ACM Trans. Program. Lang. Syst.|volume=4|number=2|pages=258–282|date=Apr 1982|doi=10.1145/357162.357169}}</ref> 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'',''[[Lisp (programming language)#Lists|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 [[term (logic)|finite terms]]; sin embargo, tiene una solución única { ''y'' ↦ ''cons''(2,''cons''(2,''cons''(2,...))) } en el conjunto de [[Tree (set theory)|á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 [[Asociatividad (álgebra)|asociativa]]; el mismo problema, visto en un [[grupo abeliano]] donde (⋅) también es considerada [[Conmutatividad|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]],<ref>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.</ref><ref>{{cite report | author1=Claus-Peter Wirth |  author2=Jörg Siekmann | author3= Christoph Benzmüller | author4= Serge Autexier | title=Lectures on Jacques Herbrand as a Logician | institution=DFKI | type=SEKI Report | number=SR-2009-01 | year=2009 | arxiv=0902.4682 }} Here: p.56</ref><ref>{{cite thesis | type=Ph.D. thesis | url=http://www.numdam.org/issue/THESE_1930__110__1_0.pdf | author=Jacques Herbrand | title=Recherches sur la théorie de la demonstration | institution=Université de Paris | series=A | volume=1252 | year=1930 }} Here: p.96-97</ref> pero la primera investigación formal puede ser atribuida a [[J. Alan Robinson|John Alan Robinson]],<ref name="Robinson.1965">{{cite journal | author=J.A. Robinson | title=A Machine-Oriented Logic Based on the Resolution Principle | journal=Journal of the ACM | volume=12 | number=1 | pages=23–41 |date=Jan 1965 | doi=10.1145/321250.321253}}; Here: sect.5.8, p.32</ref><ref>{{cite journal | author=J.A. Robinson | title=Computational logic: The unification computation | journal=Machine Intelligence | volume=6 | pages=63–72 | url=http://aitopics.org/sites/default/files/classic/Machine%20Intelligence%206/MI6-Ch4-Robinson.pdf | year=1971 }}</ref> quien utilizó unificación sintáctica de primer orden como base en su procedimiento de [[Resolución (lógica)| resolución]] de [[lógica de primer orden]], un gran paso adelante en la tecnología de [[Razonamiento automático|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 [[Sitema de tipos|tipos]], especialmente en algoritmos de [[inferencia de tipos]] basados en [[Hindley–Milner]]. Unificación semántica es utilizada en solucionadores de [[Teorías de satisfacibilidad módulo|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 [[Protocolo criptográfico|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 <math>V</math> de '''variables'''. Para unificación de orden superior es conveniente escoger un  <math>V</math> diferente de un conjunto de [[Cálculo lambda#Variables libres y ligadas|variables ligadas en expresiones lambda]].
* Un conjunto <math>T</math> de '''términos''' tales que <math>V \subseteq T</math>. Para unificaciones de primer orden y unificaciones de orden superior, <math>T</math> 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'': <math>T \rightarrow</math> [[Conjunto potencia|ℙ]]<math>(V)</math>, asignando a cada término <math>t</math> el conjunto <math>\text{vars}(t) \subsetneq V</math> de '''variables libres''' en <math>t</math>.
* Una '''[[relación de equivalencia]]''' <math>\equiv</math> on <math>T</math>, indicando que términos son considerados iguales. En unificación de orden superior, usualmente <math>t\equiv u</math> si <math>t</math> y <math>u</math> son [[Cálculo lambda#α-conversión|alpha equivalentes]]. En E-Unificación de primer orden, <math>\equiv</math> refleja el conocimiento previo sobre ciertas funciones; por ejemplo, si <math>\oplus</math> es considerado conmutativo, <math>t\equiv u</math> si <math>u</math> es el resultado de <math>t</math> intercambiando  los argumentos de <math>\oplus</math> con algunas (posiblemente todas) las ocurrencias.<ref group=note>E.g. ''a'' ⊕ (''b'' ⊕ ''f''(''x'')) ≡ ''a'' ⊕ (''f''(''x'') ⊕ ''b'') ≡ (''b'' ⊕ ''f''(''x'')) ⊕ ''a'' ≡ (''f''(''x'') ⊕ ''b'') ⊕ ''a''</ref> 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 [[Sentencia (lógica))|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 <math>V</math> de variables, un conjunto <math>C</math> de constantes y varios conjuntos <math>F_n</math> de ''n'' funciones, también llamados operadores, por cada número natural <math>n \geq 1</math>, el conjunto de términos (de primero orden sin clasificar) <math>T</math> se [[Definición recursiva|define recursivamente]] como el conjunto más pequeño con las siguientes propiedades:<ref>{{cite book| author1=C.C. Chang |author1link= Chen Chung Chang|author2= H. Jerome Keisler| author2link=Howard Jerome Keisler| title=Model Theory| year=1977| volume=73| publisher=North Holland|  series=Studies in Logic and the Foundation of Mathematics}}; here: Sect.1.3</ref>
* Cada variable es un término: <math>V \subseteq T</math>,
* Cada constante es un término: <math>C \subseteq T</math>,
* A partir de cada ''n'' términos <math>t_1, ... t_n</math>, y cada ''n'' función <math>f \in F_n</math>, se puede crear un término más grande <math>f(t_1, ..., t_n)</math>.
Por ejemplo, si <math>x\in V</math> es una variable, <math>1\in C</math> es una constante, y <math>\text{add} \in F_2</math> es una función binaria, entonces <math>x\in T, 1\in T</math>, y (por lo tanto) <math>\text{add}(x, 1) \in T</math> por la primera, segunda y tercera regla de construcción de términos respectivamente. El último término se escribe usualmente como <math>x+1</math>, 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 ===
{{AP|Cálculo lambda}}

=== Sustitución ===
'''Sustitución''' es un mapeo  <math>\sigma: V\rightarrow T</math> desde variables hacia terms; la notación <math> \{x_1\mapsto t_1, ..., x_k \mapsto t_k\}</math> se refiere a una sustitución mapeando cada variable <math>x_i</math> con el término <math>t_i</math>, para  <math>i=1,...,k</math>, y cada otra variable consigo misma. '''Aplicar''' esa sustitución a un término <math>t</math> se escribe utilizando [[Notación polaca inversa|notación de posfijo]]:  <math>t \{x_1 \mapsto t_1, ..., x_k \mapsto t_k\}</math>; que significa reemplazar (simultáneamente) cada ocurrencia la variable <math>x_i</math> en el término <math>t</math> con <math>t_i</math>. El resultado <math>t\tau</math> de haber aplicado una sustitución <math>\tau</math> a un término <math>t</math> se llama una '''instancia''' de ese término <math>t</math>.
Un ejemplo de primer orden, aplicando la sustitución {{math|{''x'' ↦ ''h''(''a'',''y''), ''z'' ↦ ''b'' }}} al término 
{|
|-
|
| <math>f(</math>
| align="center" | <math>\textbf{x}</math>
| <math>, a, g(</math>
| <math>\textbf{z}</math>
| <math> ), y)</math>
|-
| resulta en &nbsp;
|-
|
| <math>f(</math>
| <math>\textbf{h}(\textbf{a}, \textbf{y})</math>
| <math>, a, g(</math>
| <math>\textbf{b}</math>
| <math>), y).</math>
|}

=== Generalización, especialización ===

Si un término <math>t</math> tiene una instancia  equivalente a un término <math>u</math>, esto es, si <math>t\sigma \equiv u</math> por alguna sustitución <math>\sigma</math>, entonces se dice que <math>t</math> es '''más general''' que <math>u</math>, y que <math>u</math> es '''más especial''' que, o '''subsumido''' por, <math>t</math>. Por ejemplo, <math>x\oplus a</math> es más general que <math>a\oplus b</math> si ⊕ es [[Conmutatividad|conmutativa]], considerando que <math>(x\oplus a) \{x\mapsto b\} = b\oplus a\equiv a\oplus b</math>.

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, 

<math>f(x_1, a, g(z_1), y_1)</math>
es una variante de 
<math>f(x_2, a, g(z_2), y_2)</math>,
dado que

<!---Templates apparently don't accept "}" and "=" in its argument--->
<div style="text-align: center">
<math>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) </math>
</div>
y 
<div style="text-align: center">
<math>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)</math>.
</div>

Sin embargo, <math>f(x_1, a, g(z_1), y_1)</math>  ''no'' es una variante de <math>f(x_2, a, g(x_2), x_2)</math>, 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 <math>\equiv</math> arbitraria, un término puede ser más general o más específico que un término estructuralmente diferente. Por ejemplo, si ⊕ es [[Idempotencia|idempotente]], esto es, si siempre <math>x \oplus x \equiv x</math>, entonces el término <math>x\oplus y</math> es más general que <math>z</math>,<ref group=note>Considerando que <math>(x\oplus y) \{x\mapsto z, y \mapsto z\} = z\oplus z \equiv z</math></ref> y viceversa,<ref group=note>Dado que {{math|1=''z'' {''z'' ↦ ''x'' ⊕ ''y''} = ''x'' ⊕ ''y''}}</ref> a pesar de que <math>x\oplus y</math> y <math>z</math> tienen una estructura diferente.

Una sustitución <math>\sigma</math> es '''más especial''' que, o '''subsumida''' por, una sustitución <math>\tau</math> si <math>t\sigma</math> is más especial que <math>t\tau</math> para cada término <math>t</math>.  Se dice también que <math>\tau</math> es más general que <math>\sigma</math>. Por ejemplo <math> \{x \mapsto a, y \mapsto a \}</math> es más especial que <math>\tau = \{x\mapsto y\}</math>, pero <math>\sigma = \{x\mapsto a\}</math> no lo es, porque  <math>f(x, y)\sigma = f(a, y)</math> no es más especial que <math>f(x, y) \tau = f(y, y)</math>.<ref>K.R. Apt. "From Logic Programming to Prolog", p. 24.  Prentice Hall, 1997.</ref>

=== Problema de unificación, conjunto de soluciones ===

Un '''problema de unificación''' es un conjunto finito {{math|{''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub> }}} de ecuaciones potenciales, donde {{math|''l''<sub>''i''</sub>, ''r''<sub>''i''</sub> ∈ ''T''}}. Una sustitución σ es una '''solución''' de este problema si {{math|''l''<sub>''i''</sub>σ ≡ ''r''<sub>''i''</sub>σ}} para <math>i = 1, ..., n</math>. Tal sustitución se llama también un '''unificador''' del problema de unificación.
Por ejemplo, if ⊕ is [[Asociatividad (álgebra)|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 ==
[[File:Triangle diagram of syntactic unification svg.svg|thumb|Diagrama esquemático triangular de la unificación sintáctica de términos ''t''<sub>1</sub> and ''t''<sub>2</sub> 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''<sub>''n''</sub> de ''n'' funciones) y en que ≡ es una ''igualdad sintáctica''. En este esquema, cada problema de unificación  {{math|{''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub>}}} que tenga solución tiene un conjunto de soluciones unitario {{math|1={''σ''}}} que es completo y obviamente mínimo. El miembro {{mvar|σ}} es llamado '''unificador más general''' ('''mgu''' por sus siglas en inglés<ref group=NT>En el texto se utilizarán las siglas en inglés</ref>) 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 {{math|1=''l''<sub>1</sub>''σ'' = ''r''<sub>1</sub>''σ'' ∧ ... ∧ ''l''<sub>''n''</sub>''σ'' = ''r''<sub>''n''</sub>''σ''}}. Cualquier unificador del problema es subsumido<ref group=note>Formalmente: cada unificador τ satisface {{math|1=∀''x'': ''xτ'' = (''xσ'')''ρ''}} por alguna sustitución ρ</ref> por el mgu {{mvar|σ}}. El mgu es único: si '' S '' <sub> 1 </sub> y '' S '' <sub> 2 </sub> son conjuntos de soluciones completos y mínimos del mismo problema de unificación sintáctica, entonces '' S '' <sub> 1 </sub> = {'' σ '' <sub> 1 </sub>} y '' S '' <sub> 2 </sub> = {'' σ ''<sub> 2 </sub>} para algunas sustituciones {{math | 1 =''σ''<sub> 1 </sub>}} y {{math | 1 =''σ''<sub> 2 </sub>,}} y {{math | 1 = '' xσ '' <sub> 1 </sub>}} es una variante de {{math | 1 = '' xσ '' <sub> 2 </sub>}} 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''(''x''<sub>1</sub>), ''y'' ↦ ''f''(''f''(''x''<sub>1</sub>)), ''z'' ↦ ''f''(''x''<sub>1</sub>) }, { ''x'' ↦ ''f''(''f''(''x''<sub>1</sub>)), ''y'' ↦ ''f''(''f''(''f''(''x''<sub>1</sub>))), ''z'' ↦ ''f''(''f''(''x''<sub>1</sub>)) }, 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 ===

{{Quote box|title=Algoritmo de unificación Robinson (1965)|quote={{ocultar |Algoritmo de unificación Robinson (1965) |
Los símbolos se ordenan tal que las variables preceden a las funciones. Los términos se ordenan de acuerdo con su extensión y términos de igual tamaño se ordenan [[Orden lexicográfico order|lexicográficamente]].{{refn|Robinson (1965);<ref name="Robinson.1965"/> nr.2.5, 2.14, p.25}} Para un conjunto ''T'' de términos, la ruta de desacuerdo ''p'' es la ruta lexicográficamente mínima donde dos términos miembros de ''T'' difieren. Su conjunto de desacuerdos es el conjunto de subtérminos que inician en ''p'', formalmente: {{math|{ ''t''[[term (logic)#Operations with terms|{{pipe}}<sub>''p''</sub>]] : <math>t\in T</math> }}}.{{refn|Robinson (1965);<ref name="Robinson.1965"/> nr.5.6, p.32}}

'''Algoritmo:'''{{refn|Robinson (1965);<ref name="Robinson.1965"/> nr.5.8, p.32}}

 Dado un conjunto ''T'' de términos para ser unificados
 Sea <math>\sigma</math> inicialmente la sustitución identidad.
 
 '''hacer''' '''para siempre'''
   '''si''' <math>T\sigma</math> es un conjunto unitario '''entonces'''
     '''devuelva''' <math>\sigma</math>
   '''fin-si''' 
   
   sea ''D'' el conjunto de desacuerdos de <math>T\sigma</math>
   sea ''s'', ''t'' los dos términos lexicográficamente menores en ''D''
   
   '''si''' ''s'' no es una variable '''o''' ''s'' está en ''t'' '''entonces'''
     '''devuelva''' "NOUNIFICABLE"
   '''fin-si''' 
   <math>\sigma := \sigma \{ s \mapsto t \}</math>
 '''final'''
}}
}}
El primer algoritmo dado por Robinson (1965) era bastante ineficiente; cf. box.
Luego hubo un algoritmo más eficiente originado en  Martelli, Montanari (1982).<ref group=note>Alg.1, p.261. Su regla '''(a)''' corresponde con la regla '''intercambiar''', '''(b)''' con '''borrar''', '''(c)''' con '''descomponer''' y '''conflicto''', y '''(d)''' con '''eliminar''' y '''revisar'''.</ref> Este documento también enlista otros intentos previos para encontrar un algoritmo de unificación sintáctica más eficiente,<ref>{{cite report | author=Lewis Denver Baxter | title=A practically linear unification algorithm | publisher=Univ. of Waterloo, Ontario | type=Res. Report | volume=CS-76-13 | url=https://cs.uwaterloo.ca/research/tr/1976/CS-76-13.pdf |date=Feb 1976 }}</ref><ref>{{cite thesis | author=Gérard Huet | title=Resolution d'Equations dans des Langages d'Ordre 1,2,...ω | publisher=Universite de Paris VII | type=These d'etat |date=Sep 1976 | author-link=Gérard Huet }}</ref><ref name="Martelli.Montanari.1976">{{cite report | author1=Alberto Martelli | author2=Ugo Montanari | lastauthoramp=yes | title=Unification in linear time and space: A structured presentation | publisher=Consiglio Nazionale delle Ricerche, Pisa | type=Internal Note | volume=IEI-B76-16 | url=http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html | date=Jul 1976 | fechaacceso=15 de octubre de 2020 | fechaarchivo=15 de enero de 2015 | urlarchivo=https://web.archive.org/web/20150115070153/http://puma.isti.cnr.it/publichtml/section_cnr_iei/cnr_iei_1976-B4-041.html }}</ref><ref name="Paterson.Wegman.1978">{{cite journal | author=[[Michael Stewart Paterson]] and M.N. Wegman | title=Linear unification | journal=J. Comput. Syst. Sci. | volume=16 | number=2 | pages=158–167 |date=Apr 1978 | doi = 10.1016/0022-0000(78)90043-0 }}</ref><ref>{{cite book | author=J.A. Robinson |chapter= Fast unification | editor= [[Woodrow W. Bledsoe]], Michael M. Richter| title=Proc. Theorem Proving Workshop Oberwolfach | series=Oberwolfach Workshop Report | volume=1976/3 | chapter-url= http://oda.mfo.de/bsz325106819.html |date=Jan 1976 |author-link= J.A. Robinson }}</ref><ref>{{cite journal | author=M. Venturini-Zilli | title=Complexity of the unification algorithm for first-order expressions |journal= Calcolo | volume=12 |number=4 |pages= 361–372 |date= Oct 1975 | doi=10.1007/BF02575754| s2cid=189789152 }}</ref> y afirma que los algoritmos de tiempo lineal fueron descubiertos independientemente por Martelli, Montanari (1976)<ref name="Martelli.Montanari.1976"/> y Paterson, Wegman (1978).<ref name="Paterson.Wegman.1978"/>{{refn|See Martelli, Montanari (1982),<ref name="Martelli.Montanari.1982"/> sect.1, p.259. El documento de Paterson y Wegman está fechado en 1978, pero el editor de la revista lo recibió en septiembre 1976.|group=note}}

Dado un conjunto finito <math>G = \{ s_1 \doteq t_1, ..., s_n \doteq t_n \}</math> de ecuaciones potenciales, el algoritmo aplica reglas para transformarlo en un conjunto de ecuaciones equivalentes, de la forma { ''x''<sub>1</sub> ≐ ''u''<sub>1</sub>, ..., ''x''<sub>''m''</sub> ≐ ''u''<sub>''m''</sub> } donde ''x''<sub>1</sub>, ..., ''x''<sub>''m''</sub> son variables diferentes y ''u''<sub>1</sub>, ..., ''u''<sub>''m''</sub> son términos que no contienen a ninguna de las  ''x''<sub>''i''</sub>. 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.

:{|
| align="right" | <math>G \cup \{ t \doteq t \}</math>
| <math>\Rightarrow</math>
| <math>G</math>
|
| &nbsp; &nbsp; '''borrar'''
|-
| align="right" | <math>G \cup \{ f(s_0, ..., s_k) \doteq f(t_0, ..., t_k) \}</math>
| <math>\Rightarrow</math> 
| <math>G \cup \{ s_0 \doteq t_0, ..., s_k \doteq t_k \}</math>
|
| &nbsp; &nbsp; '''descomponer'''
|-
| align="right" | <math>G \cup \{ f(s_0, \ldots,s_k) \doteq g(t_0,...,t_m) \}</math>
| <math>\Rightarrow</math>
| <math>\bot</math>
| align="right" | if <math>f \neq g</math> or <math>k \neq m</math>
| &nbsp; &nbsp; '''conflicto'''
|-
| align="right" | <math>G \cup \{ f(s_0,...,s_k) \doteq x \}</math>
| <math>\Rightarrow</math>
| <math>G \cup \{ x \doteq f(s_0,...,s_k) \}</math>
|
| &nbsp; &nbsp; '''intercambio'''
|-
| align="right" | <math>G \cup \{ x \doteq t \}</math>
| <math>\Rightarrow</math>
| <math>G\{x \mapsto t\} \cup \{ x \doteq t \}</math>
| align="right" | if <math>x \not\in \text{vars}(t)</math> and <math>x \in \text{vars}(G)</math>
| &nbsp; &nbsp; '''eliminar'''<ref group="note">Aunque la regla mantiene ''x'' ≐ ''t'' en ''G'', no puede repetirse para siempre ya que la precondición ''x''∈''vars''(''G'') se invalida en la primara aplicación. En forma más general, se garantiza que el algoritmo siempre finalice, véase  [[#Prueba de finalización|más abajo]].</ref>
|-
| align="right" | <math>G \cup \{ x \doteq f(s_0,...,s_k) \}</math>
| <math>\Rightarrow</math>
| <math>\bot</math>
| align="right" | if <math>x \in \text{vars}(f(s_0,...,s_k))</math>
| &nbsp; &nbsp; '''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 <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> donde {{math|''n''<sub>''var''</sub>}} es el número de variables que ocurren más de una vez en el conjunto de ecuaciones, {{math|''n''<sub>''lhs''</sub>}} es el número de símbolos de función y constantes en el lado izquierdo de las ecuaciones potenciales, y {{math|''n''<sub>''eqn''</sub>}} es el número de ecuaciones. Cuando se aplica la regla ''eliminar'', {{math|''n''<sub>''var''</sub>}} disminuye, ya que ''x'' se elimina de ''G'' y permanece solo en {''x''≐''t''}. La aplicación de cualquier otra regla nunca puede aumentar {{math|''n''<sub>''var''</sub>}} nuevamente. Cuando se aplica la regla ''descomponer'', ''conflicto'' o ''intercambio'', {{math|''n''<sub>''lhs''</sub>}} 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 {{math|''n''<sub>''lhs''</sub>}}, pero disminuye {{math|''n''<sub>''eqn''</sub>}}. Por lo tanto, cualquier aplicación de las reglas disminuye el triple <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> con respecto al [[orden lexicográfico]], que es posible solo un número finito de veces.

[[Conor McBride]] observa<ref>{{cite journal|last=McBride|first=Conor|title=First-Order Unification by Structural Recursion|journal=Journal of Functional Programming|date=October 2003|volume=13|issue=6|pages=1061–1076|doi=10.1017/S0956796803004957|url=http://strictlypositive.org/unify.ps.gz|accessdate=2012-03-30|issn=0956-7968|citeseerx=10.1.1.25.1516}} </ref> 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 [[Inducción estructural|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.
{| class="wikitable"
|-
! Notación Prolog !! Notación Matemática !! Sustitución  !! Explicación
|-
| <code> a = a </code> || { ''a'' = ''a'' } ||  {}  || Exitoso. ([[tautología]])
|-
| <code> a = b </code> || { ''a'' = ''b'' }  || ⊥ || ''a'' y ''b'' no coinciden
|-
| <code> X = X </code> || { ''x'' = ''x'' } || {} || Exitoso. ([[tautología]])
|-
| <code> a = X </code> || { ''a'' = ''x'' }  || { ''x'' ↦ ''a'' } || ''x'' es unificada con la constante ''a''
|-
| <code> X = Y </code> || { ''x'' = ''y'' }  || { ''x'' ↦ ''y'' } || ''x'' e ''y'' son seudónimos
|-
| <code> f(a,X) = f(a,b) </code> || { ''f''(''a'',''x'') = ''f''(''a'',''b'') } ||  { ''x'' ↦ ''b'' } || símbolos de función y de constante coinciden, ''x'' es unificada con la constante ''a''
|-
| <code> f(a) = g(a) </code> || { ''f''(''a'') = ''g''(''a'') }  || ⊥ || ''f'' y ''g'' no coinciden
|-
| <code> f(X) = f(Y) </code> || { ''f''(''x'') = ''f''(''y'') } || { ''x'' ↦ ''y'' } || ''x'' e ''y'' son seudónimos
|-
| <code> f(X) = g(Y) </code> || { ''f''(''x'') = ''g''(''y'') } || ⊥ || ''f'' y ''g'' no coinciden
|-
| <code> f(X) = f(Y,Z) </code> || { ''f''(''x'') = ''f''(''y'',''z'') } || ⊥ || Fallo. Los símbolos de función '' f '' tienen diferente cantidad de argumentos
|-
| <code> f(g(X)) = f(Y) </code> || { ''f''(''g''(''x'')) = ''f''(''y'') } || { ''y'' ↦ ''g''(''x'') } || Unifica ''y'' con el término <math>g(x)</math>
|-
| <code> f(g(X),X) = f(Y,a) </code> || { ''f''(''g''(''x''),''x'') = ''f''(''y'',''a'') } || { ''x'' ↦ ''a'', ''y'' ↦ ''g''(''a'') } || Unifica ''x'' con la constante ''a'', y ''y'' con el término <math>g(a)</math>
|-
| <code> X = f(X) </code> || { ''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 <code>x=f(f(f(f(...))))</code>.
|-
| <code> X = Y, Y = a </code> || { ''x'' = ''y'', ''y'' = ''a'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || Ambos ''x'' y ''y'' son unificados con la constante ''a''
|-
| <code> a = Y, X = Y </code> || { ''a'' = ''y'', ''x'' = ''y'' } || { ''x'' ↦ ''a'', ''y'' ↦ ''a'' } || Tal como se muestra arriba (no importa el orden de las ecuaciones en el conjunto)
|-
| <code> X = a, b = X </code> || { ''x'' = ''a'', ''b'' = ''x'' }  || ⊥ || Falla. ''a'' y ''b'' no coinciden, por lo tanto  ''x'' no se puede unificar con ninguno de los dos
|}

[[File:Unification exponential blow-up svg.svg|thumb|Dos términos con un árbol exponencialmente más grande para su instancia menos común. Su representación [[Grafo acíclico dirigido|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 {{mvar|n}} puede tener un tamaño de {{math|2<sup>''n''</sup>}}. Por ejemplo, el problema <math> (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) </math> tiene el unificador más general <math> z \mapsto a,  y \mapsto a*a,  x \mapsto (a*a)*(a*a),  w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) </math>, 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.{{refn|e.g. Paterson, Wegman (1978),<ref name="Paterson.Wegman.1978"/> sect.2, p.159}}

== Notas ==
{{Reflist|group=note}}

== Notas de traducción ==
{{Reflist|group=NT}}

== Referencias ==
{{reflist}}

{{Control de autoridades}}
[[Categoría:Programación lógica]]
[[Categoría:Teoría de tipos]]