Unificación (ciencias de la computación)

De Wikipedia, la enciclopedia libre
Ir a la navegación Ir a la búsqueda

En lógica y en ciencias de la computación, unificación es un proceso algorítmico para resolución de equaciones 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 conjnto de equaciones (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 equación literlmente 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.[note 1][1]​ 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[2]​ 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 ganeral.

Por ejemplo, usando x,y,z como variables, el conjunto de equaciones 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, ycons(2,nil) } como única solución. El problema de unificación sintáctico de primer ordern { y = cons(2,y) } no tiene solución en el conjunto finite terms; sin embargo, tiene una solución única { ycons(2,cons(2,cons(2,...))) } en el conjunto de árboles infinitos. El problema de unificación semántica de primer ordern { ax = xa } tiene cualquier sustitucón de la forma { xa⋅...⋅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 cualqier sustitucion como una solución. El conjunto unitario { a = y(x) } es un problema de unficación sintáctico de segundo orden dado que y es una variable que representa una función. Una solución es { xa, 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,[3][4][5]​ pero la primera investigación formal puede ser atribuida a John Alan Robinson,[6][7]​ 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érmios. El razonamieno automático es todavía el área donde la unficiació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 (rescritura de términos) y en análisys 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 usadas en la implementación de algunos lenguajes de programación, tales como lambdaProlog, porque a pesar 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[editar]

Prerrequisitos[editar]

Formalmente, un enfoque de unificación presupone:

  • Un conjunto infinito de variables. Para unificiació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 order y unificaciones de ordern 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 order superior, usualmente si y son alpha equivalentes. En E-Unificación de primer ordern, 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 occurrences. [note 2]​Si no hay conocimiento previo del todo, entonces solo términos literalmente, o sintácticamente, idénticos son considerados iguales; en este caso, ≡ is llamado teoría libre (porque es un obbjeto 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[editar]

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:[8]

  • Cada variable es un término: ,
  • Cada constante es un térmio: ,
  • 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 , uando 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[editar]

Sustitución[editar]

substitution 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 con sigo misma. Aplicar esa sustitución a un término se escribe utilizando notación de posfijo: ; que significa reemplazar (simultáneamente) cada ocurencia la variable en el término con . El resultado de haber aplicacdo una sustitución a un término se llama una instancia de ese término . Un ejemplo de primer orden, aplicando la sustitución {xh(a,y), zb } al término

resulta en  

Generalización, especialización[editar]

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 is 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 structuralmente diferente. Por ejemplo, si ⊕ es idempotente, esto es, si siempre , entonces el término es más general que ,[note 3]​ y viceversa,[note 4]​ a pesar que y tienen una estructura diferente.

Una sustitución es más especial que, or 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 special que , pero no lo es, porque no es más especial que .[9]

Problema de unificación, conjunto de soluciones[editar]

Un problema de unificación es un conjunto finito {l1r1, ..., lnrn } de equaciones potenciales, donde li, riT. Una sustitución σ es una solución de este problema si liσ ≡ riσ para . Tal sustitución se llama tambíen un unificador del problema de unificación. Por ejemplo, if ⊕ is asociativa, el problema de unificación { xaax } tiene las soluciones {xa}, {xaa}, {xaaa}, etc., mientras que el problema { xaa } 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[editar]

Diagrama esquemático triangular de la unificación sintáctica de términos t1 and t2 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 conjnto 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 {l1r1, ..., lnrn} 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és[NT 1]​) del problema. Los términos izquierdo y derecho de cada equación potencial se vuelven sintácticamente iguales cuando se aplica el mgu, por ejemplo l1σ = r1σ ∧ ... ∧ lnσ = rnσ. Cualquier unificador del problema es subsumido[note 5]​ 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 σ 1 y σ 2 , y 1 es una variante de 2 para cada variable x que ocurra en el problema.

Por ejemplo, el problema de unificación { xz, yf(x) } tiene un unificador { xz, yf(z) }, porque

x { xz, yf(z) } = z = z { xz, yf(z) } , y
y { xz, yf(z) } = f(z) = f(x) { xz, yf(z) } .

Este es también el unificador más general. Otros unificadores para el mismo problemas son { xf(x1), yf(f(x1)), zf(x1) }, { xf(f(x1)), yf(f(f(x1))), zf(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[editar]

El primer algoritmo dado por Robinson (1965) era bastane ineficiente; cf. box. Luego hubo un algoritmo más eficiente originado en Martelli, Montanari (1982).[note 6]​ Este documento también enlista otros intentos previos para enconrar un algoritmo de unificación sintáctica más eficiente,[13][14][15][16][17][18]​ y afirma que los algoritmos de tiempo lineal fueron descubiertos independientemene por Martelli, Montanari (1976)[15]​ y Paterson, Wegman (1978).[16][note 7]

Dado un conjunto finito de ecuaciones potenciales, el algoritmo aplica reglas para transformarlo en un conjunto de equaciones equivalentes, de la forma { x1u1, ..., xmum } donde x1, ..., xm son variables diferentes y u1, ..., um son términos que no cntienen a ninguna de las xi. Un conjunto de esta forma puede ser una sustitución. Si no hay solución el algoritmo termina con ⊥; otros autores usan "Ω", "{}", or "fallo". La acción de sustituir todas las ocurrencias de x en un problema G con el término t se denota G {xt}. Por simplicidad, las constantes se Para simplificar, los símbolos constantes se consideran símbolos de función que tienen cero argumentos.

    borrar
    descomponer
if or     conflicto
    intercambio
if and     eliminar[note 8]
if     check

Revisión de ocurrencia[editar]

El intento de unificar una variable x con un término que contenga x como un subtérmino estricto xf(..., x, ...) podría genear un término infinito como solución de para x, dado que x puede aparecer como un subtérmino de si mismo. La equación xf(..., 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 xvars(t). La revisión de ocurrencia es omitida en la mayoría de los sisemas Prolog porque hace que el algoritmo se vuelva lento.

Prueba de finalización[editar]

Para la prueba de finalización del algoritmo, considere un triple donde nvar es el número de variables que ocurren más de una vez en el conjunto de ecuaciones, nlhs es el número de símbolos de función y constantes en el lado izquierdo de las ecuaciones potenciales, y neqn es el número de ecuaciones. Cuando se aplica la regla eliminar, nvar disminuye, ya que x se elimina de G y permanece solo en {xt}. La aplicación de cualquier otra regla nunca puede aumentar nvar nuevamente. Cuando se aplica la regla descomponer, conflicto o intercambio, nlhs 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 nlhs, pero disminuye neqn. Por lo tanto, cualquier aplicación de las reglas disminuye el triple con respecto al orden lexicográfico, que es posible solo un número finito de veces.

Conor McBride observa [19]​ 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 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[editar]

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.

Notación Prolog Notación Matemática Sustitución Explicación
a = a { a = a } {} Exitoso. (tautología)
a = b { a = b } a y b no coinciden
X = X { x = x } {} Exitoso. (tautología)
a = X { a = x } { xa } x es unificada con la constante a
X = Y { x = y } { xy } x e y son seudónimos
f(a,X) = f(a,b) { f(a,x) = f(a,b) } { xb } símbolos de función y de constante coinciden, x es unificada con la constante a
f(a) = g(a) { f(a) = g(a) } f y g no coinciden
f(X) = f(Y) { f(x) = f(y) } { xy } x e y son seudónimos
f(X) = g(Y) { f(x) = g(y) } f y g no coinciden
f(X) = f(Y,Z) { f(x) = f(y,z) } Fallo. Los símbolos de función f tienen diferente cantidad de argumentos
f(g(X)) = f(Y) { f(g(x)) = f(y) } { yg(x) } Unifica y con el término
f(g(X),X) = f(Y,a) { f(g(x),x) = f(y,a) } { xa, yg(a) } Unifica x con la constante a, y y con el término
X = f(X) { 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 x=f(f(f(f(...)))).

X = Y, Y = a { x = y, y = a } { xa, ya } Ambos x y y son unificados con la constante a
a = Y, X = Y { a = y, x = y } { xa, ya } Tal como se muestra arriba (no importa el orden de las equaciones en el conjunto)
X = a, b = X { x = a, b = x } Falla. a y b no coinciden, por lo tanto x no se puede unificar con ninguno de los dos
Dos términos con un árbol exponencialmente más grande para su instancia menos común. Su represetación 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 n puede tener un tamaño de 2n. Por ejemplo, el problema tiene el unificador más general , 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.[20]

Notas[editar]

  1. en este caso, todavía exise un conjunto completo de sustituciones (por ejemplo: el conjunto de todas las soluciones); sin embargo, cada una de estas solucioes contiene miembros redundantes.
  2. E.g. a ⊕ (bf(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (bf(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a
  3. Considerando que
  4. Dado que z {zxy} = xy
  5. Formalmente: cada unificador τ satisface x: = ()ρ por alguna sustitución ρ
  6. Alg.1, p.261. Su regla (a) corresponde con la regla intercambiar, (b) con borrar, (c) con descomponer y conflicto, y (d) con eliminar and revisar.
  7. See Martelli, Montanari (1982),[2]​ sect.1, p.259. El documento de Paterson y Wegman está fechado en 1978; sin embargo, el editor de la revista lo recibió en septiembre 1976.
  8. Aunque la regla mantiene xt en G, no puede repetirse para siempre ya que la precondición xvars(G) se invalida en la primara aplicación. En forma más general, se garantiza que el algoritmo siempre finalice, véase más abajo.

Notas de traducción[editar]

  1. En el texto se utilizarán las siglas en inglés

Referencias[editar]

  1. Fages, François; Huet, Gérard (1986). «Complete Sets of Unifiers and Matchers in Equational Theories». Theoretical Computer Science 43: 189-200. doi:10.1016/0304-3975(86)90175-1. 
  2. a b Martelli, Alberto; Montanari, Ugo (Apr 1982). «An Efficient Unification Algorithm». ACM Trans. Program. Lang. Syst. 4 (2): 258-282. doi:10.1145/357162.357169. 
  3. 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.
  4. Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009), Lectures on Jacques Herbrand as a Logician (SEKI Report) (SR-2009-01), DFKI, arXiv:0902.4682  Here: p.56
  5. Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (Ph.D. thesis). A 1252. Université de Paris.  Here: p.96-97
  6. a b c d J.A. Robinson (Jan 1965). «A Machine-Oriented Logic Based on the Resolution Principle». Journal of the ACM 12 (1): 23-41. doi:10.1145/321250.321253. ; Here: sect.5.8, p.32
  7. J.A. Robinson (1971). «Computational logic: The unification computation». Machine Intelligence 6: 63-72. 
  8. C.C. Chang; H. Jerome Keisler (1977). Model Theory. Studies in Logic and the Foundation of Mathematics 73. North Holland. ; here: Sect.1.3
  9. K.R. Apt. "From Logic Programming to Prolog", p. 24. Prentice Hall, 1997.
  10. Robinson (1965);[6]​ nr.2.5, 2.14, p.25
  11. Robinson (1965);[6]​ nr.5.6, p.32
  12. Robinson (1965);[6]​ nr.5.8, p.32
  13. Lewis Denver Baxter (Feb 1976), A practically linear unification algorithm (Res. Report), CS-76-13, Univ. of Waterloo, Ontario 
  14. Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (These d'etat). Universite de Paris VII. 
  15. a b Alberto Martelli & Ugo Montanari (Jul 1976), Unification in linear time and space: A structured presentation (Internal Note), IEI-B76-16, Consiglio Nazionale delle Ricerche, Pisa 
  16. a b c Michael Stewart Paterson and M.N. Wegman (Apr 1978). «Linear unification». J. Comput. Syst. Sci. 16 (2): 158-167. doi:10.1016/0022-0000(78)90043-0. 
  17. J.A. Robinson (Jan 1976). «Fast unification». En Woodrow W. Bledsoe, Michael M. Richter, ed. Proc. Theorem Proving Workshop Oberwolfach. Oberwolfach Workshop Report. 1976/3. 
  18. M. Venturini-Zilli (Oct 1975). «Complexity of the unification algorithm for first-order expressions». Calcolo 12 (4): 361-372. doi:10.1007/BF02575754.  Parámetro desconocido |s2cid= ignorado (ayuda)
  19. McBride, Conor (October 2003). «First-Order Unification by Structural Recursion». Journal of Functional Programming 13 (6): 1061-1076. ISSN 0956-7968. doi:10.1017/S0956796803004957. Consultado el 30 March 2012.  Parámetro desconocido |citeseerx= ignorado (ayuda)
  20. e.g. Paterson, Wegman (1978),[16]​ sect.2, p.159