Unification (computer science)

Formalmente, un enfoque de unificación presupone

• Un conjunto infinito${\displaystyle V}$de variables . Para una unificación de orden superior, es conveniente elegir${\displaystyle V}$disjunto del conjunto de variables ligadas de términos lambda .
• Un conjunto${\displaystyle T}$de términos tales que${\displaystyle V\subseteq T}$. Para la unificación de primer orden,${\displaystyle T}$es normalmente el conjunto de términos de primer orden (términos construidos a partir de símbolos de variables y funciones). Para la unificación de orden superior${\displaystyle T}$Consta de términos de primer orden y términos lambda (términos que contienen algunas variables de orden superior).
• Un mapeo${\displaystyle {\text{vars}}\colon T\rightarrow }$${\displaystyle \mathbb {P} }$${\displaystyle (V)}$, asignando a cada término${\displaystyle t}$el conjunto${\displaystyle {\text{vars}}(t)\subsetneq V}$de variables libres que ocurren en${\displaystyle t}$.
• Una teoría o relación de equivalencia${\displaystyle \equiv }$en${\displaystyle T}$, indicando qué términos se consideran iguales. Para la E-unificación de primer orden,${\displaystyle \equiv }$refleja el conocimiento previo sobre ciertos símbolos de función; por ejemplo, si${\displaystyle \oplus }$se considera conmutativo,${\displaystyle t\equiv u}$si${\displaystyle u}$resultados de${\displaystyle t}$intercambiando los argumentos de${\displaystyle \oplus }$en algunas (posiblemente todas) las ocurrencias. ^{[ nota 1 ]} En el caso más típico en el que no hay ningún conocimiento previo, entonces solo se consideran iguales los términos idénticos literal o sintácticamente. En este caso, ≡ se denomina teoría libre (porque es un objeto libre ), teoría vacía (porque el conjunto de oraciones de igualdad , o el conocimiento previo, está vacío), teoría de funciones no interpretadas (porque la unificación se realiza sobre términos no interpretados ) o teoría de constructores (porque todos los símbolos de función simplemente construyen términos de datos, en lugar de operar sobre ellos). Para la unificación de orden superior, generalmente${\displaystyle t\equiv u}$si${\displaystyle t}$y${\displaystyle u}$son alfa equivalentes .

Como ejemplo de cómo el conjunto de términos y la teoría afectan al conjunto de soluciones, el problema de unificación sintáctica de primer orden { y = cons (2, y ) } no tiene solución sobre el conjunto de términos finitos . Sin embargo, tiene la única solución { y ↦ cons (2, cons (2, cons (2,...))) } sobre el conjunto de términos de árbol infinitos . De manera similar, el problema de unificación semántica de primer orden { a ⋅ x = x ⋅ a } tiene cada sustitución de la forma { x ↦ a ⋅...⋅ a } como solución en un semigrupo , es decir, si (⋅) se considera asociativo . Pero el mismo problema, visto en un grupo abeliano , donde (⋅) también se considera conmutativo , tiene cualquier sustitución como solución.

Como ejemplo de unificación de orden superior, el conjunto unitario { a = y ( x ) } es un problema de unificación sintáctica de segundo orden, ya que y es una variable de función. Una solución es { x ↦ a , y ↦ ( función identidad ) }; otra es { y ↦ ( función constante que asigna cada valor a a ), x ↦ (cualquier valor) }.

Una sustitución es una asignación${\displaystyle \sigma :V\rightarrow T}$de variables a términos; la notación${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$se refiere a una asignación de sustitución para cada variable${\displaystyle x_{i}}$al término${\displaystyle t_{i}}$, para${\displaystyle i=1,...,k}$y cualquier otra variable a sí misma; la${\displaystyle x_{i}}$deben ser distintos por pares. Aplicando esa sustitución a un término${\displaystyle t}$se escribe en notación posfija como${\displaystyle t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$; significa reemplazar (simultáneamente) cada aparición de cada variable${\displaystyle x_{i}}$en el término${\displaystyle t}$por${\displaystyle t_{i}}$El resultado${\displaystyle t\tau }$de aplicar una sustitución${\displaystyle \tau }$a un término${\displaystyle t}$se denomina un ejemplo de ese término${\displaystyle t}$. Como ejemplo de primer orden, aplicando la sustitución { x ↦ h ( a , y ), z ↦ b } al término

Si un término${\displaystyle t}$tiene una instancia equivalente a un término${\displaystyle u}$, es decir, si${\displaystyle t\sigma \equiv u}$por alguna sustitución${\displaystyle \sigma }$, entonces${\displaystyle t}$se llama más general que${\displaystyle u}$, y${\displaystyle u}$se denomina más especial que, o subsumido por,${\displaystyle t}$. Por ejemplo,${\displaystyle x\oplus a}$es más general que${\displaystyle a\oplus b}$si ⊕ es conmutativo , ya que entonces${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$.

Si ≡ es la identidad literal (sintáctica) de términos, un término puede ser a la vez más general y más especial que otro solo si ambos términos difieren únicamente en sus nombres de variables, no en su estructura sintáctica; tales términos se denominan variantes o renombramientos entre sí. Por ejemplo, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ es una variante de ${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$, desde $${\displaystyle 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})}$$ y $${\displaystyle 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}).}$$ Sin embargo,${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$no es una variante de ${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$Dado que ninguna sustitución puede transformar el segundo término en el primero, el segundo término es, por lo tanto, más especial que el primero.

Para arbitrario${\displaystyle \equiv }$, un término puede ser a la vez más general y más especial que un término estructuralmente diferente. Por ejemplo, si ⊕ es idempotente , es decir, si siempre${\displaystyle x\oplus x\equiv x}$, entonces el término${\displaystyle x\oplus y}$es más general que${\displaystyle z}$, ^{[ nota 2 ]} y viceversa, ^{[ nota 3 ]} aunque${\displaystyle x\oplus y}$y${\displaystyle z}$son de diferente estructura.

Una sustitución${\displaystyle \sigma }$es más especial que, o está subsumido por, una sustitución${\displaystyle \tau }$si${\displaystyle t\sigma }$está subsumido por${\displaystyle t\tau }$para cada término${\displaystyle t}$También decimos que${\displaystyle \tau }$es más general que${\displaystyle \sigma }$. De forma más formal, tomemos un conjunto infinito no vacío.${\displaystyle V}$de variables auxiliares tales que ninguna ecuación${\displaystyle l_{i}\doteq r_{i}}$en el problema de unificación contiene variables de${\displaystyle V}$Luego una sustitución${\displaystyle \sigma }$queda subsumido por otra sustitución.${\displaystyle \tau }$si hay una sustitución${\displaystyle \theta }$de tal manera que para todos los términos${\displaystyle X\notin V}$,${\displaystyle X\sigma \equiv X\tau \theta }$. ^{[ 2 ]} Por ejemplo${\displaystyle \{x\mapsto a,y\mapsto a\}}$está subsumido por${\displaystyle \tau =\{x\mapsto y\}}$, usando${\displaystyle \theta =\{y\mapsto a\}}$, pero ${\displaystyle \sigma =\{x\mapsto a\}}$no está subsumido por${\displaystyle \tau =\{x\mapsto y\}}$, como${\displaystyle f(x,y)\sigma =f(a,y)}$no es un caso de ${\displaystyle f(x,y)\tau =f(y,y)}$. ^{[ 3 ]}

Una sustitución σ es una solución del problema de unificación E si l _i σ ≡ r _i σ para${\displaystyle i=1,...,n}$. Dicha sustitución también se denomina unificador de E. Por ejemplo, si ⊕ es asociativo , 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 E dado , un conjunto S de unificadores se denomina completo si cada sustitución de solución está incluida en alguna sustitución de S. Siempre existe un conjunto de sustitución completo (por ejemplo, el conjunto de todas las soluciones), pero en algunos marcos (como la unificación de orden superior sin restricciones) el problema de determinar si existe alguna solución (es decir, si el conjunto de sustitución completo no está vacío) es indecidible.

El conjunto S se llama mínimo si ninguno de sus miembros engloba a otro. Dependiendo del marco, un conjunto de sustitución completo y mínimo puede tener cero, uno, un número finito o infinito de miembros, o puede no existir en absoluto debido a una cadena infinita de miembros redundantes. ^{[ 4 ]} Por lo tanto, en general, los algoritmos de unificación calculan una aproximación finita del conjunto completo, que puede o no ser mínimo, aunque la mayoría de los algoritmos evitan los unificadores redundantes cuando es posible. ^{[ 2 ]} Para la unificación sintáctica de primer orden, Martelli y Montanari ^{[ 5 ]} dieron un algoritmo que informa la insolubilidad o calcula un único unificador que por sí mismo forma un conjunto de sustitución completo y mínimo, llamado el unificador más general .

Jacques Herbrand analizó los conceptos básicos de la unificación y esbozó un algoritmo en 1930. ^{[ 9 ] [ 10 ] [ 11 ]} Pero la mayoría de los autores atribuyen el primer algoritmo de unificación a John Alan Robinson (véase el recuadro). ^{[ 12 ] [ 13 ] [ nota 5 ]} El algoritmo de Robinson tenía un comportamiento exponencial en el peor de los casos, tanto en el tiempo como en el espacio. ^{[ 11 ] [ 15 ]} Numerosos autores han propuesto algoritmos de unificación más eficientes. ^{[ 16 ]} Los algoritmos con comportamiento de tiempo lineal en el peor caso fueron descubiertos independientemente por Martelli y Montanari (1976) y Paterson y Wegman (1976) ^{[ nota 6 ]} Baader y Snyder (2001) utiliza una técnica similar a la de Paterson-Wegman, por lo tanto es lineal, ^{[ 17 ]} pero como la mayoría de los algoritmos de unificación de tiempo lineal es más lento que la versión de Robinson en entradas de tamaño pequeño debido a la sobrecarga del preprocesamiento de las entradas y el posprocesamiento de la salida, como la construcción de una representación DAG . de Champeaux (2022) también tiene una complejidad lineal en el tamaño de la entrada pero es competitivo con el algoritmo de Robinson en entradas de tamaño pequeño. La aceleración se obtiene utilizando una representación orientada a objetos del cálculo de predicados que evita la necesidad de pre y posprocesamiento, haciendo en cambio que los objetos variables sean responsables de crear una sustitución y de lidiar con el aliasing. De Champeaux afirma que la capacidad de agregar funcionalidad al cálculo de predicados representado como objetos programáticos brinda oportunidades para optimizar también otras operaciones lógicas. ^{[ 15 ]}

El siguiente algoritmo se presenta comúnmente y proviene de Martelli y Montanari (1982) . ^{[ nota 7 ]} Dado un conjunto finito${\displaystyle G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}}$de ecuaciones potenciales, el algoritmo aplica reglas para transformarlo en un conjunto equivalente de ecuaciones de la forma { x ₁ ≐ u ₁ , ..., x _m ≐ u _m } donde x ₁ , ..., x _m son variables distintas y u ₁ , ..., u _m son términos que no contienen ninguno de los x _i . Un conjunto de esta forma puede leerse como una sustitución. Si no hay solución, el algoritmo termina con ⊥; otros autores usan "Ω" o " fail " en ese caso. La operación de sustituir todas las ocurrencias de la variable x en el problema G con el término t se denota G { x ↦ t }. Para simplificar, los símbolos constantes se consideran símbolos de función con cero argumentos.

En la sintaxis de Prolog, un símbolo que comienza con mayúscula es un nombre de variable; un símbolo que comienza con minúscula es un símbolo de función; la coma se usa como operador lógico AND . En notación matemática , x, y, z se usan como variables, f, g como símbolos de función y a, b como constantes.

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 2 ⁿ . Por ejemplo, el problema ⁠${\displaystyle (((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))}$Tiene el unificador más general .${\displaystyle \{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))\}}$⁠ , cf. imagen. Para evitar la complejidad temporal exponencial causada por tal explosión, los algoritmos de unificación avanzados trabajan con grafos acíclicos dirigidos (DAG) en lugar de árboles. ^{[ 19 ]}

El concepto de unificación es una de las ideas principales de la programación lógica . Específicamente, la unificación es un componente básico de la resolución , una regla de inferencia para determinar la satisfacibilidad de una fórmula. En Prolog , el símbolo de igualdad =implica una unificación sintáctica de primer orden. Representa el mecanismo de vinculación del contenido de las variables y puede considerarse como una asignación única.

En Prolog:

1. Una variable puede unificarse con una constante, un término u otra variable, convirtiéndose así efectivamente en su alias. En muchos dialectos modernos de Prolog y en la lógica de primer orden , una variable no puede unificarse con un término que la contenga; esta es la llamada comprobación de ocurrencias .
2. Dos constantes solo pueden unificarse si son idénticas.
3. De forma similar, un término puede unificarse con otro si los símbolos de función principales y las aridades de ambos términos son idénticos y si los parámetros pueden unificarse simultáneamente. Cabe destacar que se trata de un comportamiento recursivo.
4. La mayoría de las operaciones, incluidas +, -, *, /, no son evaluadas por =. Por ejemplo, 1+2 = 3no es satisfacible porque son sintácticamente diferentes. El uso de restricciones aritméticas enteras #=introduce una forma de E-unificación para la cual estas operaciones son interpretadas y evaluadas. ^{[ 20 ]}

Los algoritmos de inferencia de tipos se basan típicamente en la unificación, en particular la inferencia de tipos de Hindley-Milner que utilizan los lenguajes funcionales Haskell y ML . Por ejemplo, al intentar inferir el tipo de la expresión de Haskell , el compilador utilizará el tipo de la función de construcción de listas , el tipo del primer argumento y el tipo del segundo argumento . La variable de tipo polimórfico se unificará con y el segundo argumento se unificará con . no puede ser ambos y al mismo tiempo, por lo tanto, esta expresión no está correctamente tipada.True : ['x']a -> [a] -> [a](:)BoolTrue[Char]['x']aBool[a][Char]aBoolChar

Al igual que en Prolog, se puede proporcionar un algoritmo para la inferencia de tipos:

1. Cualquier variable de tipo se unifica con cualquier expresión de tipo y se instancia según esa expresión. Una teoría específica podría restringir esta regla con una comprobación de ocurrencia.
2. Dos constantes de tipo se unifican solo si son del mismo tipo.
3. Dos construcciones de tipos se unifican solo si son aplicaciones del mismo constructor de tipos y todos sus tipos componentes se unifican recursivamente.

La unificación se ha utilizado en diferentes áreas de investigación de la lingüística computacional. ^{[ 21 ] [ 22 ]}

Se dice que una teoría es decidible si se ha diseñado un algoritmo de unificación que finaliza para cualquier problema de entrada. Se dice que una teoría es semidecidible si se ha diseñado un algoritmo de unificación que finaliza para cualquier problema de entrada resoluble , pero que puede seguir buscando indefinidamente soluciones para un problema de entrada irresoluble.

La unificación es decidible para las siguientes teorías:

• A ^{[ 26 ]}
• A , C ^{[ 27 ]}
• A , C , I ^{[ 28 ]}
• A , C , N _l ^{[ nota 9 ] [ 28 ]}
• A , yo ^{[ 29 ]}
• A , N _l , N _r (monoide) ^{[ 30 ]}
• C ^{[ 28 ]}
• Anillos booleanos ^{[ 31 ] [ 32 ]}
• Grupos abelianos , incluso si la signatura se expande con símbolos adicionales arbitrarios (pero no axiomas) ^{[ 33 ].}
• Álgebras modales K4 ^{[ 34 ]}

La unificación es semidecidible para las siguientes teorías:

• A , D _l , Dr ^{[ 35 ]}_​
• A , C , D _l ^{[ nota 9 ] [ 36 ]}
• Anillos conmutativos ^{[ 33 ]}

Si hay un sistema de reescritura de términos convergente R disponible para E , el algoritmo de paramodulación unilateral ^{[ 37 ]} se puede utilizar para enumerar todas las soluciones de ecuaciones dadas.

Partiendo de G como el problema de unificación a resolver y S como la sustitución identidad, se aplican reglas de forma no determinista hasta que el conjunto vacío aparece como el G real , en cuyo caso el S real es una sustitución unificadora. Dependiendo del orden en que se aplican las reglas de paramodulación, de la elección de la ecuación real de G y de la elección de las reglas de R en mutate , son posibles diferentes rutas de cálculo. Solo algunas conducen a una solución, mientras que otras terminan en un G ≠ {} donde no se aplica ninguna otra regla (por ejemplo, G = { f (...) ≐ g (...) }).

Por ejemplo, se utiliza un sistema de reescritura de términos R que define el operador de adición de listas construidas a partir de cons y nil ; donde cons ( x , y ) se escribe en notación infija como x . y para abreviar; por ejemplo, app ( a . b . nil , c . d . nil ) → a . app ( b . nil , c . d . nil ) → a . b . app ( nil , c . d . nil ) → a . b . c . d . nil demuestra la concatenación de las listas a . b . nil y c . d . nil , empleando la regla de reescritura 2,2 y 1. La teoría ecuacional E correspondiente a R es el cierre de congruencia de R , ambos vistos como relaciones binarias sobre términos. Por ejemplo, app ( a . b . nil , c . d . nil ) ≡ a . b . c . d . nil ≡ app ( a . b . c . d . nil , nil ). El algoritmo de paramodulación enumera soluciones a ecuaciones con respecto a esa E cuando se le proporciona el ejemplo R .

A continuación se muestra un ejemplo exitoso de ruta de cálculo para el problema de unificación { app ( x , app ( y , x )) ≐ a . a . nil }. Para evitar conflictos de nombres de variables, las reglas de reescritura se renombran consistentemente cada vez antes de su uso por regla mutate ; v ₂ , v ₃ , ... son nombres de variables generados por computadora para este propósito. En cada línea, la ecuación elegida de G se resalta en rojo. Cada vez que se aplica la regla mutate , la regla de reescritura elegida ( 1 o 2 ) se indica entre paréntesis. De la última línea, se puede obtener la sustitución unificadora S = { y ↦ nil , x ↦ a . nil }. De hecho, app ( x , app ( y , x )) { y ↦ nil , x ↦ a . nil } = app ( a . nil , app ( nil , a . nil )) ≡ app ( a . nil , a . nil ) ≡ a . app ( nil , a . nil ) ≡ a . a . nil resuelve el problema dado. Una segunda ruta de cálculo exitosa, obtenible al elegir "mutate(1), mutate(2), mutate(2), mutate(1)", conduce a la sustitución S = { y ↦ a . a . nil , x ↦ nil }; no se muestra aquí. Ninguna otra ruta conduce al éxito.

Si R es un sistema de reescritura de términos convergente para E , un enfoque alternativo a la sección anterior consiste en la aplicación sucesiva de " pasos de estrechamiento "; esto eventualmente enumerará todas las soluciones de una ecuación dada. Un paso de estrechamiento (véase la imagen) consiste en

• escogiendo un subtérmino no variable del término actual,
• unificándolo sintácticamente con el lado izquierdo de una regla de R y
• reemplazar el lado derecho de la regla instanciada en el término instanciado.

Formalmente, si l → r es una copia renombrada de una regla de reescritura de R , que no tiene variables en común con un término s , y el subtérmino s | _p no es una variable y es unificable con l a través del mgu σ , entonces s puede reducirse al término t = sσ [ rσ ] _p , es decir, al término sσ , con el subtérmino en p reemplazado por rσ . La situación en la que s puede reducirse a t se denota comúnmente como s ↝ t . Intuitivamente, una secuencia de pasos de estrechamiento t ₁ ↝ t ₂ ↝ ... ↝ t _n puede pensarse como una secuencia de pasos de reescritura t ₁ → t ₂ → ... → t _n , pero con el término inicial t ₁ instanciado cada vez más, según sea necesario para que cada una de las reglas utilizadas sea aplicable.

El ejemplo de cálculo de paramodulación anterior corresponde a la siguiente secuencia de estrechamiento ("↓" indica instanciación aquí):

El último término, v ₂ . v ₂ . nil, puede unificarse sintácticamente con el término original del lado derecho a . a . nil .

El lema de estrechamiento ^{[ 38 ]} garantiza que siempre que una instancia de un término s pueda ser reescrita a un término t por un sistema de reescritura de términos convergente, entonces s y t pueden ser estrechados y reescritos a un término s ′ y t ′ , respectivamente, de tal manera que t ′ sea una instancia de s ′ .

Formalmente: siempre que sσ → ∗ t se cumpla para alguna sustitución σ, entonces existen términos s ′ , t ′ tales que s ↝ ∗ s ′ y t → ∗ t ′ y s ′ τ = t ′ para alguna sustitución τ.