En lógica e informática , específicamente en razonamiento automatizado , la unificación es un proceso algorítmico de resolución de ecuaciones entre expresiones simbólicas , cada una de las cuales tiene la forma Lado izquierdo = Lado derecho . Por ejemplo, usando x , y , z como variables y tomando f como una función no interpretada , el conjunto de ecuaciones singleton { f (1, y ) = f ( x ,2)} es un problema sintáctico de unificación de primer orden que tiene la sustitución { x ↦ 1, y ↦ 2 } como única solución.
Las convenciones difieren sobre qué valores pueden asumir las variables y qué expresiones se consideran equivalentes. En la unificación sintáctica de primer orden, las variables abarcan términos de primer orden y la equivalencia es sintáctica. Esta versión de unificación tiene una "mejor" respuesta única y se utiliza en programación lógica e implementación de sistemas de tipos de lenguajes de programación , especialmente en algoritmos de inferencia de tipos basados en Hindley-Milner . En la unificación de orden superior, posiblemente restringida a la unificación de patrones de orden superior , los términos pueden incluir expresiones lambda y la equivalencia depende de la reducción beta. Esta versión se utiliza en asistentes de prueba y programación lógica de orden superior, por ejemplo Isabelle , Twelf y lambdaProlog . Finalmente, en la unificación semántica o E-unificación, la igualdad está sujeta a conocimientos previos y las variables abarcan una variedad de dominios. Esta versión se utiliza en solucionadores SMT , algoritmos de reescritura de términos y análisis de protocolos criptográficos .
Un problema de unificación es un conjunto finito E ={ l 1 ≐ r 1 , ..., l n ≐ r n } de ecuaciones a resolver, donde l i , r i están en el conjunto de términos o expresiones . Dependiendo de qué expresiones o términos se permiten que aparezcan en un conjunto de ecuaciones o un problema de unificación, y qué expresiones se consideran iguales, se distinguen varios marcos de unificación. Si en una expresión se permiten variables de orden superior, es decir, variables que representan funciones , el proceso se denomina unificación de orden superior ; de lo contrario, unificación de primer orden . Si se requiere una solución para hacer que ambos lados de cada ecuación sean literalmente iguales, el proceso se llama unificación sintáctica o libre ; de lo contrario, unificación semántica o ecuacional , o unificación E , o teoría del módulo de unificación .
Si el lado derecho de cada ecuación es cerrado (sin variables libres), el problema se llama coincidencia (de patrón) . El lado izquierdo (con variables) de cada ecuación se llama patrón . [1]
Formalmente, un enfoque de unificación presupone
Como ejemplo de cómo el conjunto de términos y la teoría afecta el 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 una solución única { 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 (⋅) se considera también conmutativo , tiene cualquier sustitución como solución.
Como ejemplo de unificación de orden superior, el conjunto singleton { a = y ( x ) } es un problema sintáctico de unificación de segundo orden, ya que y es una variable de función. Una solución es { x ↦ a , y ↦ ( función identidad ) }; otro es { y ↦ ( función constante que asigna cada valor a a ), x ↦ (cualquier valor) }.
Una sustitución es un mapeo de variables a términos; la notación se refiere a una sustitución que asigna cada variable al término , for y todas las demás variables a sí misma; deben ser distintos por pares. La aplicación de esa sustitución a un término se escribe en notación postfija como ; significa reemplazar (simultáneamente) cada aparición de cada variable en el término por . El resultado de aplicar una sustitución a un término se denomina instancia de ese término . Como ejemplo de primer orden, aplicando la sustitución { x ↦ h ( a , y ), z ↦ b } al término
Si un término tiene una instancia equivalente a un término , es decir, si se trata de alguna sustitución , entonces se le llama más general que , y se le llama más especial que, o subsumido por ,. Por ejemplo, es más general que si ⊕ es conmutativo , desde entonces .
Si ≡ es identidad literal (sintáctica) de términos, un término puede ser más general y más especial que otro sólo si ambos términos difieren sólo en sus nombres de variables, no en su estructura sintáctica; dichos términos se denominan variantes o cambios de nombre entre sí. Por ejemplo, es una variante de , ya que y Sin embargo, no es una variante de , ya que ninguna sustitución puede transformar el último término en el primero. Por tanto, este último término es propiamente más especial que el primero.
Para arbitrario , 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 , entonces el término es más general que , [nota 2] y viceversa, [nota 3] aunque y sean de diferente estructura.
Una sustitución es más especial o está subsumida por una sustitución si está subsumida por para cada término . También decimos que es más general que . Más formalmente, tome un conjunto infinito no vacío de variables auxiliares tal que ninguna ecuación en el problema de unificación contenga variables de . Entonces una sustitución es subsumida por otra sustitución si hay una sustitución tal que para todos los términos , . [2] Por ejemplo, está subsumido por , usando , pero no está subsumido por , ya que no es una instancia de . [3]
Una sustitución σ es una solución del problema de unificación E si l i σ ≡ r i σ para . Esta 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 dado E , un conjunto S de unificadores se llama completo si cada sustitución de solución está subsumida por alguna sustitución en 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 irrestricta de orden superior) 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 subsume a otro. Dependiendo del marco, un conjunto de sustitución completo y mínimo puede tener cero, uno, un número finito o un número infinito de miembros, o puede no existir en absoluto debido a una cadena infinita de miembros redundantes. [4] Así, en general, los algoritmos de unificación calculan una aproximación finita del conjunto completo, que puede ser mínima o no, aunque la mayoría de los algoritmos evitan 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 unificador único que por sí mismo forma un conjunto de sustitución mínimo y completo, llamado el unificador más general .
La unificación sintáctica de términos de primer orden es el marco de unificación más utilizado. Se basa en que T es el conjunto de términos de primer orden (sobre un conjunto dado V de variables, C de constantes y F n de símbolos de funciones n -arias) y en que ≡ es la igualdad sintáctica . En este marco, cada problema de unificación resoluble { l 1 ≐ r 1 , ..., l n ≐ r n } tiene un conjunto de soluciones singleton completo, y obviamente mínimo, { σ } . Su miembro σ se denomina unificador más general ( mgu ) del problema. Los términos en el lado izquierdo y derecho de cada ecuación potencial se vuelven sintácticamente iguales cuando se aplica mgu, es decir, l 1 σ = r 1 σ ∧ ... ∧ l n σ = r n σ . Cualquier unificador del problema está subsumido [nota 4] por el mgu σ . El mgu es único hasta las variantes: si S 1 y S 2 son conjuntos de solución 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 xσ 1 es una variante de xσ 2 para cada variable x que ocurre en el problema.
Por ejemplo, el problema de unificación { x ≐ z , y ≐ f ( x ) } tiene un unificador { x ↦ z , y ↦ f ( z ) }, porque
Este es también el unificador más general. Otros unificadores para el mismo problema son, por ejemplo, { x ↦ f ( x 1 ), y ↦ f ( f ( x 1 ) ), z ↦ f ( x 1 ) }, { x ↦ f ( f ( x 1 ) ), y ↦ f ( f ( f ( x 1 )) ), z ↦ f ( f ( x 1 )) }, y así sucesivamente; hay infinitos unificadores similares.
Como otro ejemplo, el problema g ( x , x ) ≐ f ( y ) no tiene solución con respecto a que ≡ sea identidad literal, ya que cualquier sustitución aplicada al lado izquierdo y derecho mantendrá los g y f más externos , respectivamente, y Los términos con diferentes símbolos de función más externos son sintácticamente diferentes.
Los símbolos están ordenados de manera que las variables preceden a los símbolos de función. Los términos se ordenan aumentando la extensión escrita; Los términos igualmente largos se ordenan lexicográficamente . [6] Para un conjunto T de términos, su camino de desacuerdo p es el camino lexicográficamente mínimo donde dos términos miembros de T difieren. Su conjunto de desacuerdo es el conjunto de subtérminos que comienzan en p , formalmente: { t | pag : }. [7]
Algoritmo: [8]
Given a set T of terms to be unified
Let initially be the identity substitutiondo forever
if
is a singleton setthen
return
fi
let D be the disagreement set of
let s, t be the two lexicographically least terms in D
if
s is not a variableor
s occurs in tthen
return
"NONUNIFIABLE"
fi
done
Jacques Herbrand discutió los conceptos básicos de 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 (ver recuadro). [12] [13] [nota 5] El algoritmo de Robinson tuvo el peor comportamiento exponencial tanto en el tiempo como en el espacio. [11] [15] Numerosos autores han propuesto algoritmos de unificación más eficientes. [16] Martelli y Montanari (1976) y Paterson y Wegman (1976) descubrieron de forma independiente algoritmos con el peor comportamiento en tiempo lineal. [nota 6] Baader y Snyder (2001) utilizan una técnica similar a la de Paterson-Wegman, por lo que 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 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 complejidad lineal en el tamaño de entrada, pero es competitivo con el algoritmo de Robinson en entradas de tamaño pequeño. La aceleración se obtiene mediante el uso de una representación orientada a objetos del cálculo de predicados que evita la necesidad de procesamiento previo y posterior, haciendo que los objetos variables sean responsables de crear una sustitución y de lidiar con el alias. de Champeaux afirma que la capacidad de agregar funcionalidad al cálculo de predicados representado como objetos programáticos también brinda oportunidades para optimizar otras operaciones lógicas. [15]
El siguiente algoritmo se presenta comúnmente y se origina en Martelli y Montanari (1982). [nota 7] Dado un conjunto finito de ecuaciones potenciales, el algoritmo aplica reglas para transformarlo en un conjunto equivalente de ecuaciones de la forma { x 1 ≐ u 1 , ..., x m ≐ u m } donde x 1 , . .., x m son variables distintas y u 1 , ..., 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 utilizan "Ω", o " fallar " en ese caso. La operación de sustituir todas las apariciones de la variable x en el problema G con el término t se denota G { x ↦ t }. Por simplicidad, los símbolos constantes se consideran símbolos de funciones que tienen cero argumentos.
Un intento de unificar una variable x con un término que contenga a x como un subtérmino estricto x ≐ f (..., x , ...) conduciría a un término infinito como solución para x , ya que x ocurriría como un subtérmino de sí mismo . En el conjunto de términos (finitos) de primer orden definidos anteriormente, la ecuación x ≐ f (..., x , ...) no tiene solución; por lo tanto, la regla de eliminación sólo puede aplicarse si x ∉ vars ( t ). Dado que esa verificación adicional, llamada verificación de ocurrencia , ralentiza el algoritmo, se omite, por ejemplo, en la mayoría de los sistemas Prolog. Desde un punto de vista teórico, omitir la verificación equivale a resolver ecuaciones sobre árboles infinitos, consulte #Unificación de términos infinitos a continuación.
Para la prueba de terminación del algoritmo, considere una tripleta donde n var es el número de variables que ocurren más de una vez en el conjunto de ecuaciones, n lhs es el número de símbolos de función y constantes en el lado izquierdo de las ecuaciones potenciales, y n eqn es el número de ecuaciones. Cuando se aplica la regla de eliminación , n var disminuye, ya que x se elimina de G y se mantiene solo en { x ≐ t }. La aplicación de cualquier otra regla nunca podrá volver a aumentar n var . Cuando se aplica la regla de descomposición , conflicto o intercambio , n lhs disminuye, ya que al menos la f más externa del lado izquierdo desaparece. La aplicación de cualquiera de las reglas restantes, eliminar o verificar, no puede aumentar n lhs , pero disminuye n eqn . De ahí que cualquier aplicación de regla disminuya el triple respecto del orden lexicográfico , lo cual es posible sólo un número finito de veces.
Conor McBride observa [18] que "al expresar la estructura que explota la unificación" en un lenguaje de tipo dependiente como Epigram , el algoritmo de unificación de Robinson puede volverse recursivo en el número de variables , en cuyo caso una prueba de terminación separada se vuelve innecesaria.
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 y . 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.
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 n . Por ejemplo, el problema tiene el unificador más general , cf. imagen. Para evitar la complejidad temporal exponencial causada por tal explosión, los algoritmos de unificación avanzados funcionan en gráficos acíclicos dirigidos (dags) en lugar de árboles. [19]
El concepto de unificación es una de las ideas principales detrás 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 la 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 verse como una especie de asignación única.
En prólogo:
+
, -
, *
, /
, no son evaluadas por =
. Entonces, por ejemplo, 1+2 = 3
no es satisfactorio porque son sintácticamente diferentes. El uso de restricciones aritméticas de números enteros #=
introduce una forma de unificación E para la cual estas operaciones se interpretan y evalúan. [20]Los algoritmos de inferencia de tipos generalmente se basan en la unificación, particularmente la inferencia de tipos Hindley-Milner que utilizan los lenguajes funcionales Haskell y ML . Por ejemplo, al intentar inferir el tipo de expresión de Haskell True : ['x']
, el compilador utilizará el tipo a -> [a] -> [a]
de función de construcción de lista (:)
, el tipo Bool
del primer argumento True
y el tipo [Char]
del segundo argumento ['x']
. La variable de tipo polimórfico a
se unificará con Bool
y el segundo argumento [a]
se unificará con [Char]
. a
no puede ser ambas cosas Bool
al Char
mismo tiempo, por lo tanto, esta expresión no está escrita correctamente.
Al igual que Prolog, se puede proporcionar un algoritmo para la inferencia de tipos:
La unificación se ha utilizado en diferentes áreas de investigación de la lingüística computacional. [21] [22]
La lógica de ordenación permite asignar una clasificación , o tipo , a cada término y declarar una clasificación s 1 como una subclasificación de otra clasificación s 2 , comúnmente escrita como s 1 ⊆ s 2 . Por ejemplo, cuando se razona sobre criaturas biológicas, es útil declarar que un perro tipo es un subtipo de un animal tipo .se requieraun término de algún tipo s , se puede proporcionar en su lugar un término de cualquier subtipo de s . Por ejemplo, asumiendo una declaración de función madre : animal → animal , y una declaración constante lassie : perro , el término madre ( lassie ) es perfectamente válido y tiene el tipo animal . Para proporcionar la información de que la madre de un perro es a su vez un perro,se podrá emitir otra declaración madre : perro → perro ; esto se llama sobrecarga de funciones , similar a la sobrecarga en los lenguajes de programación .
Walther dio un algoritmo de unificación para términos en lógica ordenada, requiriendo que para dos tipos declarados s 1 , s 2 también se declarara su intersección s 1 ∩ s 2 : si x 1 y x 2 es una variable de tipo s 1 y s 2 , respectivamente, la ecuación x 1 ≐ x 2 tiene la solución { x 1 = x , x 2 = x }, donde x : s 1 ∩ s 2 . [23] Después de incorporar este algoritmo en un demostrador de teoremas automatizado basado en cláusulas, pudo resolver un problema de referencia traduciéndolo a lógica ordenada, reduciéndolo así a un orden de magnitud, ya que muchos predicados unarios se convirtieron en géneros.
Smolka generalizó la lógica ordenada para permitir el polimorfismo paramétrico . [24] En su marco, las declaraciones de subclasificación se propagan a expresiones de tipo complejo. Como ejemplo de programación, se puede declarar una lista de clasificación paramétrica ( X ) (siendo X un parámetro de tipo como en una plantilla de C++ ), y a partir de una declaración de subclasificación int ⊆ float la relación lista ( int ) ⊆ lista ( float ) se obtiene automáticamente. inferido, lo que significa que cada lista de números enteros es también una lista de flotantes.
Schmidt-Schauß generalizó la lógica ordenada por orden para permitir declaraciones de términos. [25] Como ejemplo, asumiendo declaraciones de subclasificación par ⊆ int e impar ⊆ int , una declaración de término como ∀ i : int . ( i + i ): incluso permite declarar una propiedad de suma de enteros que no podría expresarse mediante sobrecarga ordinaria.
Antecedentes sobre árboles infinitos:
Algoritmo de unificación, Prolog II:
Aplicaciones:
La e-unificación es el problema de encontrar soluciones a un conjunto dado de ecuaciones , teniendo en cuenta algunos conocimientos previos sobre ecuaciones E. Este último se da como un conjunto de igualdades universales . Para algunos conjuntos particulares E , se han ideado algoritmos de resolución de ecuaciones (también conocidos como algoritmos de unificación E ); para otros, se ha demostrado que tales algoritmos no pueden existir.
Por ejemplo, si a y b son constantes distintas, la ecuación no tiene solución con respecto a la unificación puramente sintáctica , donde no se sabe nada sobre el operador . Sin embargo, si se sabe que es conmutativo , entonces la sustitución { x ↦ b , y ↦ a } resuelve la ecuación anterior, ya que
El conocimiento previo E podría establecer la conmutatividad de por la igualdad universal " para todo u , v ".
Se dice que la unificación es decidible para una teoría, si se ha ideado un algoritmo de unificación que termine para cualquier problema de entrada. Se dice que la unificación es semidecidible para una teoría, si se ha ideado un algoritmo de unificación que termine para cualquier problema de entrada con solución , pero que pueda seguir buscando para siempre soluciones de un problema de entrada sin solución.
La unificación es decidible para las siguientes teorías:
La unificación es semidecidible para las siguientes teorías:
Si hay un sistema de reescritura de términos convergente R disponible para E , el algoritmo de paramodulación unilateral [38] se puede utilizar para enumerar todas las soluciones de ecuaciones dadas.
Comenzando con G como el problema de unificación a resolver y S como la sustitución de identidad, las reglas se aplican de manera 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 mutación , son posibles diferentes caminos de cálculo. Sólo algunos conducen a una solución, mientras que otros terminan en G ≠ {} donde no se aplica ninguna regla adicional (por ejemplo, G = { f (...) ≐ g (...) }).
Por ejemplo, se utiliza un término sistema de reescritura R que define el operador de adición de listas creadas a partir de cons y nil ; donde cons ( x , y ) se escribe en notación infija como x . y por brevedad; por ejemplo , aplicación ( a.b.nil , c.d.nil ) → a . aplicación ( b . nil , c . d . nil ) → a . b . aplicación ( nil , c.d.nil ) → a . b . C . d . nil demuestra la concatenación de las listas a . b . nulo y c . d . nulo , 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 en términos. Por ejemplo, aplicación ( a . b . nil , c . d . nil ) ≡ a . b . C . d . nil ≡ aplicación ( a . b . c . d . nil , nil ). El algoritmo de paramodulación enumera soluciones a ecuaciones con respecto a E cuando se alimenta con el ejemplo R.
Un ejemplo exitoso de ruta de cálculo para el problema de unificación { app ( x , app ( y , x )) ≐ a . a . nil } se muestra a continuación. Para evitar conflictos de nombres de variables, las reglas de reescritura se renombran constantemente cada vez antes de su uso mediante rule mutate ; v 2 , v 3 , ... son nombres de variables generados por computadora para este propósito. En cada línea, la ecuación elegida de G está resaltada en rojo. Cada vez que se aplica la regla de mutación , la regla de reescritura elegida ( 1 o 2 ) se indica entre paréntesis. Desde la última línea, la sustitución unificadora S = { y ↦ nil , x ↦ a . nil } se puede obtener. De hecho, app ( x , app ( y , x )) { y ↦ nil , x ↦ a . nil } = aplicación ( a . nil , aplicación ( nil , a . nil )) ≡ aplicación ( a . nil , a . nil ) ≡ a . aplicación ( nil , a.nil ) ≡ a . a . nil resuelve el problema dado. Una segunda ruta de cálculo exitosa, que se puede obtener eligiendo "mutar(1), mutar(2), mutar(2), mutar(1)" conduce a la sustitución S = { y ↦ a . a . nulo , x ↦ nulo }; no se muestra aquí. Ningún otro camino 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 (ver imagen) consiste en
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 de 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 reducción t 1 ↝ t 2 ↝ ... ↝ t n puede considerarse como una secuencia de pasos de reescritura t 1 → t 2 → ... → t n , pero con el término inicial t 1 siendo instanciados cada vez más, según sea necesario para que cada una de las reglas utilizadas sea aplicable.
El ejemplo anterior de cálculo de paramodulación corresponde a la siguiente secuencia de estrechamiento ("↓" indica creación de instancias aquí):
El último término, v 2 . v2 . nil se puede unificar sintácticamente con el término original del lado derecho a . a . nulo .
El lema de estrechamiento [39] asegura que siempre que una instancia de un término s pueda reescribirse en un término t mediante un sistema de reescritura de términos convergente, entonces s y t pueden reducirse y reescribirse en un término s ′ y t ′ , respectivamente, tales que t ′ es una instancia de s ′ .
Formalmente: siempre que sσ t es válido para alguna sustitución σ, entonces existen términos s ′ , t ′ tales que s s ′ yt t ′ y s ′ τ = t ′ para alguna sustitución τ.
Muchas aplicaciones requieren que se considere la unificación de términos lambda tipificados en lugar de términos de primer orden. Esta unificación suele denominarse unificación de orden superior . La unificación de orden superior es indecidible , [40] [41] [42] y tales problemas de unificación no tienen la mayoría de los unificadores generales. Por ejemplo, el problema de unificación { f ( a , b , a ) ≐ d ( b , a , c ) }, donde la única variable es f , tiene las soluciones { f ↦ λ x .λ y .λ z . d ( y , x , c ) }, { f ↦ λ x .λ y .λ z . re ( y , z , c ) }, { f ↦ λ x .λ y .λ z . d ( y , a , c ) }, { f ↦ λ x .λ y .λ z . re ( segundo , x , c ) }, { f ↦ λ x .λ y .λ z . d ( b , z , c ) } y { f ↦ λ x .λ y .λ z . re ( b , a , c ) }. Una rama bien estudiada de la unificación de orden superior es el problema de unificar términos lambda simplemente tipados módulo la igualdad determinada por conversiones αβη. Gérard Huet dio un algoritmo de (pre)unificación semidecidible [43] que permite una búsqueda sistemática del espacio de unificadores (generalizando el algoritmo de unificación de Martelli-Montanari [5] con reglas para términos que contienen variables de orden superior) que parece funcionar suficientemente bien en la práctica. Huet [44] y Gilles Dowek [45] han escrito artículos sobre este tema.
Varios subconjuntos de unificación de orden superior se comportan bien, ya que son decidibles y tienen un unificador más general para problemas solucionables. Uno de esos subconjuntos son los términos de primer orden descritos anteriormente. La unificación de patrones de orden superior , debida a Dale Miller, [46] es otro de esos subconjuntos. Los lenguajes de programación lógica de orden superior λProlog y Twelf han pasado de una unificación completa de orden superior a implementar solo el fragmento de patrón; Sorprendentemente, la unificación de patrones es suficiente para casi todos los programas, si cada problema de unificación que no es de patrón se suspende hasta que una sustitución posterior coloque la unificación en el fragmento de patrón. Un superconjunto de unificación de patrones llamado unificación de funciones como constructores también se comporta bien. [47] El demostrador del teorema de Zipperposition tiene un algoritmo que integra estos subconjuntos de buen comportamiento en un algoritmo completo de unificación de orden superior. [2]
En lingüística computacional, una de las teorías más influyentes de la construcción elíptica es que las elipses están representadas por variables libres cuyos valores luego se determinan mediante unificación de orden superior. Por ejemplo, la representación semántica de "A Jon le gusta Mary y a Peter también" es como ( j , m ) ∧ R( p ) y el valor de R (la representación semántica de los puntos suspensivos) está determinado por la ecuación como ( j , m ) = R( j ) . El proceso de resolución de tales ecuaciones se llama unificación de orden superior. [48]
Wayne Snyder dio una generalización tanto de la unificación de orden superior como de la unificación E, es decir, un algoritmo para unificar términos lambda módulo una teoría ecuacional. [49]
{{cite book}}
: CS1 maint: multiple names: authors list (link)