Unificación (informática)

format_list_bulleted Contenido keyboard_arrow_down

ImprimirCitar

En lógica e informática, la unificación es un proceso algorítmico de resolución de ecuaciones entre expresiones simbólicas.

Dependiendo de qué expresiones (también llamadas términos) pueden aparecer en un conjunto de ecuaciones (también llamado problema de unificación) y qué expresiones se consideran iguales, varios marcos de unificación se distinguen. 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 denomina unificación sintáctica o libre; de lo contrario, semántica o unificación ecuacional, o E-unificación, o teoría del módulo de unificación.

Una solución de un problema de unificación se denota como una sustitución, es decir, un mapeo que asigna un valor simbólico a cada variable de las expresiones del problema. Un algoritmo de unificación debe calcular para un problema determinado un conjunto de sustitución completo y mínimo, es decir, un conjunto que contenga todas las soluciones del problema y ningún miembro redundante. Dependiendo del marco, un conjunto de sustitución mínimo y completo puede tener como máximo uno, como máximo un número finito de miembros o posiblemente un número infinito de miembros, o puede no existir en absoluto. En algunos marcos, generalmente es imposible decidir si existe alguna solución. Para la unificación sintáctica de primer orden, Martelli y Montanari proporcionaron un algoritmo que informa de la imposibilidad de resolver o calcula un conjunto de sustitución de singleton completo y mínimo que contiene el denominado unificador más general.

Por ejemplo, usando x,y,z como variables, el conjunto de ecuaciones singleton { cons(x,contras(x,nil)) = contras(2,y) } es un problema de unificación sintáctica de primer orden que tiene la sustitución { x ↦ 2, y ↦ cons (2,nil) } como su única solución. 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 solución única { y ↦ cons(2,cons(2,cons(2,...))) } sobre el conjunto de árboles infinitos. 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; el mismo problema, visto en un grupo abeliano, donde (⋅) también se considera conmutativo, tiene cualquier sustitución como solución. El conjunto singleton { 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 de identidad) }; otro es { y ↦ (función constante que asigna cada valor a a), x ↦ (cualquier valor) }.

Jacques Herbrand descubrió por primera vez un algoritmo de unificación, mientras que una primera investigación formal se puede atribuir a John Alan Robinson, quien usó la unificación sintáctica de primer orden como componente básico de su procedimiento de resolución para la lógica de primer orden, un gran paso adelante en la tecnología de razonamiento automatizado, ya que eliminó una fuente de explosión combinatoria: la búsqueda de instanciación de términos. Hoy en día, el razonamiento automatizado sigue siendo la principal área de aplicación de la unificación. La unificación sintáctica de primer orden se utiliza en la programación lógica y la implementación de sistemas de tipos de lenguajes de programación, especialmente en algoritmos de inferencia de tipos basados en Hindley-Milner. La unificación semántica se utiliza en solucionadores de SMT, algoritmos de reescritura de términos y análisis de protocolos criptográficos. La unificación de orden superior se usa en asistentes de prueba, por ejemplo, Isabelle y Twelf, y formas restringidas de unificación de orden superior (unificación de patrones de orden superior) se usan en algunas implementaciones de lenguajes de programación, como lambdaProlog, como los patrones de orden superior son expresivos, su procedimiento de unificación asociado retiene propiedades teóricas más cercanas a la unificación de primer orden.

Definición formal

Requisitos

Formalmente, un enfoque de unificación presupone

Un conjunto infinito $V$ de variables. Para la unificación de orden superior, es conveniente elegir $V$ descomponerse del conjunto de variables a plazo de lambda.
Un juego $T$ de términos tales que $Vsubseteq T$ . Para la unificación de primer orden, $T$ es generalmente el conjunto de términos de primer orden (termos construidos a partir de símbolos de función y variable). Para la unificación de orden superior $T$ consiste en términos de primera orden y términos de lambda (termos que contienen algunas variables de orden superior).
Una cartografía Vars: ${displaystyle Trightarrow }$ $mathbb {P}$ $(V)$ , asignando a cada término $t$ el conjunto ${displaystyle {text{vars}}(t)subsetneq V}$ de variables libres en $t$ .
An Relación de equivalencia $equiv$ on $T$ , indicando qué términos se consideran iguales. Para la unificación E de primer orden, $equiv$ refleja el conocimiento de fondo sobre ciertos símbolos de función; por ejemplo, si $oplus$ se considera conmutativa, ${displaystyle tequiv u}$ si $u$ de los resultados $t$ intercambiando los argumentos de $oplus$ en algunas ocurrencias (posiblemente todas). En el caso más típico de que no hay ningún conocimiento de fondo, entonces sólo literalmente, o sintácticamente, los términos idénticos se consideran iguales. En este caso, se llama ≡ teoría libre (porque es un objeto libre), el teoría vacía (porque el conjunto de frases ecuales, o el conocimiento de fondo, está vacío), el teoría de las funciones no interpretadas (porque la unificación se hace en términos no interpretados) o teoría de los constructores (porque todos los símbolos de función simplemente acumulan términos de datos, en lugar de operar en ellos). Para la unificación de orden superior, generalmente ${displaystyle tequiv u}$ si $t$ y $u$ son equivalentes alfa.

Sustitución

A sustitución es una asignación ${displaystyle sigma:Vrightarrow 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 cada variable $x_{i}$ a la palabra $t_{i}$ , para ${displaystyle i=1,...,k}$ , y cada otra variable a sí misma. Aplicar esa sustitución a un plazo $t$ está escrito en notación postfix como ${displaystyle t{x_{1}mapsto t_{1},...,x_{k}mapsto t_{k}}}$ ; significa reemplazar (simultaneamente) cada ocurrencia de cada variable $x_{i}$ en el término $t$ por $t_{i}$ . El resultado ${displaystyle ttau }$ de la aplicación de una sustitución $tau$ a un plazo $t$ se llama ejemplo de ese mandato $t$ . Como ejemplo de primer orden, aplicando la sustitución ${} x \mapsto h () a, Sí.), z \mapsto b}$ a la palabra

	$f($	${textbf {x}}$	${displaystylea,g(}$	${textbf {z}}$	${displaystyle),y)}$
rendimientos
	$f($	${displaystyle {textbf {h}}({textbf {a}},{textbf {y}})}$	${displaystylea,g(}$	${textbf {b}}$	${displaystyle),y).}$

Generalización, especialización

Si un término $t$ tiene una instancia equivalente a un término $u$ , eso es, si ${displaystyle tsigma equiv u}$ para algunas sustituciones $sigma$ , entonces $t$ se llama más general que $u$ , y $u$ se llama más especial que, o subsumido por, $t$ . Por ejemplo, ${displaystyle xoplus a}$ es más general que ${displaystyle aoplus b}$ si ⊕ es conmutativo, desde entonces ${displaystyle (xoplus a){xmapsto b}=boplus aequiv aoplus b}$ .

Si literal es la identidad literal (sintáctica) de términos, un término puede ser tanto más general y más especial que otro sólo si ambos términos difieren sólo en sus nombres variables, no en su estructura sintáctica; tales términos se llaman variantes, o renombramientos uno del otro. 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 entonces

${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})}$

${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})}$ es no una variante de ${displaystyle f(x_{2},a,g(x_{2}),x_{2})}$ , ya que ninguna sustitución puede transformar este último término en el primero. Por lo tanto, este último término es adecuadamente más especial que el primero.

Para arbitrarios $equiv$ , un término puede ser tanto más general como más especial que un término estructuralmente diferente. Por ejemplo, si ⊕ es idempotente, es decir, si siempre ${displaystyle xoplus xequiv x}$ , entonces el término ${displaystyle xoplus y}$ es más general que $z$ , y viceversa, aunque ${displaystyle xoplus y}$ y $z$ son de estructura diferente.

Una sustitución $sigma$ es más especial que, o subsumido por una sustitución $tau$ si ${displaystyle tsigma }$ es más especial que ${displaystyle ttau }$ para cada mandato $t$ . También decimos que $tau$ es más general que $sigma$ . Por ejemplo ${displaystyle {xmapsto a,ymapsto a}}$ es más especial que ${displaystyle tau ={xmapsto y}}$ , pero ${displaystyle sigma ={xmapsto a}}$ no es, como ${displaystyle f(x,y)sigma =f(a,y)}$ no es más especial que ${displaystyle f(x,y)tau =f(y,y)}$ .

Problema de unificación, conjunto de soluciones

A problema de la unificación es un conjunto finito ${} l 1 ≐ r 1,... l n ≐ r n}$ de ecuaciones potenciales, donde $l i, r i ▪ T$ . Una sustitución σ es una solución de ese problema si $l i σ ngel r i σ$ para ${displaystyle i=1,...,n}$ . Tal sustitución también se llama unificador del problema de la unificación. 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, un conjunto S de unificadores se llama completo si cada sustitución de solución está subsumida por alguna sustitución σ ∈ S; el conjunto S se llama minimal si ninguno de sus miembros subsume a otro.

Unificación sintáctica de términos de primer orden

Diagrama de triángulo esquemático de términos sintacticamente unificadores t₁ y t₂ por una sustitución

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 determinado conjunto V de variables, C de constantes y F_n de n-símbolos de funciones arias) y en ≡ siendo igualdad sintáctica . En este marco, cada problema de unificación solucionable ${l 1 ≐ r 1,..., l n ≐ r n}$ tiene un conjunto de soluciones singleton completo y obviamente mínimo ${σ}$ . Su miembro $σ$ se llama el unificador más general (mgu) de el problema. Los términos del lado izquierdo y derecho de cada ecuación potencial se vuelven sintácticamente iguales cuando se aplica mgu, es decir, $l 1 σ = r 1 σ \land... \land l n σ = r n σ . Cualquier unificador del problema se incluye en mgu σ . El mgu es único hasta las variantes: si S 1 y S 2 son conjuntos de soluciones completas y mínimas de el 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 aparece en el problema.$

Por ejemplo, el problema de unificación { x ≐ z, y ≐ f(x ) } tiene un unificador { x ↦ z, y ↦ f(z ) }, porque

x	{} x ↦ z, Sí. ↦ f()z)	=	z	=	z	{} x ↦ z, Sí. ↦ f()z)	, y
Sí.	{} x ↦ z, Sí. ↦ f()z)	=	f()z)	=	f()x)	{} x ↦ z, Sí. ↦ f()z)	.

Este es también el unificador más general. Otros unificadores para el mismo problema son, p. { x ↦ f(x₁), y ↦ f (f(x₁)), z ↦ f (x₁) }, { x ↦ f(f(x₁)), y ↦ f(f(f(x₁))), z ↦ f(f(x₁)) }, 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 una 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

algoritmo de unificación de Robinson de 1965

Los símbolos se ordenan tal que las variables preceden a los símbolos de función. Los términos se ordenan aumentando la longitud escrita; términos igualmente largos se ordenan lexicográficamente. Para un set T de términos, su desacuerdo sendero p es el menos camino lexicográfico donde dos términos miembros de T difieren. Su punto de desacuerdo es el conjunto de subtermos que comienzan en p, formalmente: $tin T$ }.
Algoritmo:Given a set T of terms to be unified Let $sigma$ initially be the identity substitution do forever if ${displaystyle Tsigma }$ is a singleton set then return $sigma$ fi let D be the disagreement set of ${displaystyle Tsigma }$ let s, t be the two lexicographically least terms in D if s is not a variable or s occurs in t then return "NONUNIFIABLE" fi ${displaystyle sigma:=sigma {smapsto t}}$ done

El primer algoritmo proporcionado por Robinson (1965) era bastante ineficiente; cf. caja. El siguiente algoritmo más rápido se originó a partir de Martelli, Montanari (1982). Este documento también enumera los intentos anteriores de encontrar un algoritmo de unificación sintáctica eficiente y afirma que los algoritmos de tiempo lineal fueron descubiertos de forma independiente por Martelli, Montanari (1976) y Paterson, Wegman (1976, 1978).

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 a 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 x_i. Un conjunto de este formulario se puede leer como una sustitución. Si no hay solución el algoritmo termina con ⊥; otros autores utilizan "Ω", "{}", o "falla"en ese caso. La operación de sustitución de todas las ocurrencias de variables x en el problema G a plazo t es denotado G {}x ↦ t}. Para la simplicidad, los símbolos constantes se consideran símbolos de función que tienen cero argumentos.

${displaystyle Gcup {tdoteq t}}$	$Rightarrow$	$G$		delete
${displaystyle Gcup {f(s_{0},...,s_{k})doteq f(t_{0},...,t_{k})}}$	$Rightarrow$	${displaystyle Gcup {s_{0}doteq t_{0},...,s_{k}doteq t_{k}}}$		decompose
${displaystyle Gcup {f(s_{0},ldotss_{k})doteq g(t_{0},...,t_{m})}}$	$Rightarrow$	$bot$	if ${displaystyle fneq g}$ or ${displaystyle kneq m}$	conflict
${displaystyle Gcup {f(s_{0},...,s_{k})doteq x}}$	$Rightarrow$	${displaystyle Gcup {xdoteq f(s_{0},...,s_{k})}}$		swap
${displaystyle Gcup {xdoteq t}}$	$Rightarrow$	${displaystyle G{xmapsto t}cup {xdoteq t}}$	if ${displaystyle xnot in {text{vars}}(t)}$ and ${displaystyle xin {text{vars}}(G)}$	eliminate
${displaystyle Gcup {xdoteq f(s_{0},...,s_{k})}}$	$Rightarrow$	$bot$	if ${displaystyle xin {text{vars}}(f(s_{0},...,s_{k}))}$	check

Comprobación de eventos

Un intento de unificar una variable x con un término que contiene x como un subtérmino estricto x ≐ f (..., x,...) llevarí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 eliminar solo se puede aplicar si x ∉ vars(t). Dado que esa verificación adicional, llamada ocurre verificación, ralentiza el algoritmo, se omite, p. 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.

Prueba de rescisión

Para la prueba de terminación del algoritmo considerar un triple ${displaystyle langle n_{var},n_{lhs},n_{eqn}rangle }$ Donde $n Var$ es el número de variables que ocurren más de una vez en el conjunto de la ecuación, $n #$ es el número de símbolos de función y constantes en los lados izquierdos de las ecuaciones potenciales, y $n eqn$ es el número de ecuaciones. Cuando regla eliminar se aplica, $n Var$ disminuciones, desde x es eliminado de G y guardado sólo en x ≐ t }. Aplicar cualquier otra regla nunca puede aumentar $n Var$ otra vez. Cuando regla decompose, conflicto, o Swap se aplica, $n #$ disminuciones, ya que al menos el lado izquierdo más exterior f desaparece. Aplicar cualquiera de las reglas restantes Borrador o cheque no puede aumentar $n #$ , pero disminuye $n eqn$ . Por lo tanto, cualquier aplicación regla disminuye el triple ${displaystyle langle n_{var},n_{lhs},n_{eqn}rangle }$ con respecto al orden lexicográfico, que es posible sólo un número finito de veces.

Conor McBride observa que "al expresar la estructura que explota la unificación" en un lenguaje tipificado de forma dependiente como Epigram, el algoritmo de unificación de Robinson se puede hacer recursivo en el número de variables, en cuyo caso se vuelve innecesaria una prueba de terminación por separado.

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 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.

Notación prolog	Notación matemática	Sustitución unificadora	Explicación
`a = a`	{} a = a }	{}	Los éxitos.
`a = b`	{} a = b }	⊥	a y b no coincide
`X = X`	{} x = x }	{}	Los éxitos.
`a = X`	{} a = x }	{} x ↦ a }	x se unifica con la constante a
`X = Y`	{} x = Sí. }	{} x ↦ Sí. }	x y Sí. son alias
`f(a,X) = f(a,b)`	{} f()a,x) f()a,b)	{} x ↦ b }	función y símbolos constantes coinciden, x se unifica con la constante b
`f(a) = g(a)`	{} f()a) g()a)	⊥	f y g no coincide
`f(X) = f(Y)`	{} f()x) f()Sí.)	{} x ↦ Sí. }	x y Sí. son alias
`f(X) = g(Y)`	{} f()x) g()Sí.)	⊥	f y g no coincide
`f(X) = f(Y,Z)`	{} f()x) f()Sí.,z)	⊥	Fails. El f símbolos de función tienen diferentes aridades
`f(g(X)) = f(Y)`	{} f()g()x) = f()Sí.)	{} Sí. ↦ g()x)	Unificado Sí. con el término $g(x)$
`f(g(X),X) = f(Y,a)`	{} f()g()x),x) f()Sí.,a)	{} x ↦ a, Sí. ↦ g()a)	Unificado x con constante a, y Sí. con el término $g(a)$
`X = f(X)`	{} x = f()x)	debe ser	Devuelve ⊥ en la lógica de primera orden y muchos dialectos modernos Prolog (forzado por la El cheque). Los éxitos en Prolog tradicional y en Prolog II, unificación x con un término infinito `x=f(f(f(f(...))))`.
`X = Y, Y = a`	{} x = Sí., Sí. = a }	{} x ↦ a, Sí. ↦ a }	Ambos x y Sí. están unificados con la constante a
`a = Y, X = Y`	{} a = Sí., x = Sí. }	{} x ↦ a, Sí. ↦ a }	Como arriba (orden de ecuaciones en conjunto no importa)
`X = a, b = X`	{} x = a, b = x }	⊥	Fails. a y b no coinciden, así que x no se puede unificar con ambos

Dos términos con un árbol exponencialmente más grande para su instancia menos común. Su representación de dag (la parte más justa y naranja) sigue siendo de tamaño lineal.

El unificador más general de un problema de unificación de primer orden sintáctico de tamaño $n$ puede tener un tamaño de $2 n$ . Por ejemplo, el problema $(((a*z)*y)*x)*wdoteq w*(x*(y*(z*a)))$ tiene el unificador más general ${displaystyle {zmapsto a,ymapsto a*a,xmapsto (a*a)*(a*a),wmapsto ((a*a)*(a*a))*((a*a)*(a*a))}}$ , foto. Para evitar la complejidad del tiempo exponencial causada por tales algoritmos de unificación avanzados y soplados funcionan en gráficos acíclicos dirigidos en lugar de árboles.

Aplicación: unificación en programación lógica

El concepto de unificación es una de las ideas principales detrás de la programación lógica, más conocida a través del lenguaje Prolog. Representa el mecanismo de enlace del contenido de las variables y puede verse como una especie de asignación única. En Prolog, esta operación se indica con el símbolo de igualdad =, pero también se realiza cuando se crean instancias de variables (ver más abajo). También se usa en otros idiomas mediante el uso del símbolo de igualdad =, pero también junto con muchas operaciones, incluidas +, -, *, /. Los algoritmos de inferencia de tipos se basan normalmente en la unificación.

En Prólogo:

Una variable que no está condicionada, es decir, no se realizaron unificaciones previas en ella, puede ser unificada con un átomo, un término u otra variable no asentada, convirtiéndose así en su alias. En muchos dialectos modernos Prolog y en la lógica de primera orden, una variable no puede ser unificada con un término que la contiene; esto es lo que se llama El cheque.
Dos átomos sólo pueden ser unificados si son idénticos.
Análogamente, un término puede ser unificado con otro término si los símbolos y aridades de la función superior de los términos son idénticos y si los parámetros pueden ser unificados simultáneamente. Tenga en cuenta que esto es un comportamiento recursivo.

Aplicación: inferencia de tipos

La unificación se usa durante la inferencia de tipos, por ejemplo, en el lenguaje de programación funcional Haskell. Por un lado, el programador no necesita proporcionar información de tipo para cada función, por otro lado, se utiliza para detectar errores de escritura. La expresión de Haskell Verdadero: ['x', 'y', 'z'] no está escrita correctamente. La función de construcción de listas (:) es de tipo a -> [a] -> [a], y para el primer argumento True la variable de tipo polimórfico a tiene que estar unificada con True' tipo s, Bool. El segundo argumento, ['x', 'y', 'z'], es de tipo [Char], pero a no puede ser Bool y Char al mismo tiempo.

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

Cualquier variable de tipo unifica con cualquier tipo de expresión, y es instantánea a esa expresión. Una teoría específica podría restringir esta regla con un cheque ocurre.
Las constantes de dos tipos se unifican sólo si son del mismo tipo.
Construcciones de dos tipos unifican solamente si son aplicaciones del mismo tipo constructor y todos sus tipos de componentes recurrentemente unifican.

Debido a su naturaleza declarativa, el orden en una secuencia de unificaciones (generalmente) no es importante.

Tenga en cuenta que, en la terminología de la lógica de primer orden, un átomo es una proposición básica y se unifica de manera similar a un término de Prolog.

Aplicación: unificación de estructura de características

Consulte Feature_structure.

La unificación se ha utilizado en diferentes áreas de investigación de la lingüística computacional.

Unificación ordenada por orden

La lógica ordenada por orden permite asignar una clasificación o tipo a cada término y declarar una clasificación s₁ un subsort de otro tipo s₂, comúnmente escrito como s₁ ⊆ s₂. Por ejemplo, al razonar sobre criaturas biológicas, es útil declarar una especie perro como una subespecie de una especie animal. Siempre que se requiera un término de algún tipo s, en su lugar se puede proporcionar 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 niña: perro, el término madre(chica) es perfectamente válido y tiene el género animal. Para suministrar la información de que la madre de un perro es a su vez un perro, se puede emitir otra declaración madre: perro → perro; esto se denomina sobrecarga de funciones, similar a la sobrecarga en los lenguajes de programación.

Walther proporcionó un algoritmo de unificación para términos en lógica ordenada, requiriendo para cualquiera de los dos tipos declarados s₁, s₂ su intersección s₁ ∩ s₂ para declarar también: si x₁ y x₂ es una variable de tipo s₁ y s₂, respectivamente, la ecuación x₁ ≐ x₂ tiene la solución { x₁ = x, x₂ = x }, donde x: s₁ ∩ s₂. Después de incorporar este algoritmo en un probador de teoremas automatizado basado en cláusulas, pudo resolver un problema de referencia traduciéndolo a una lógica ordenada, reduciéndolo así a un orden de magnitud, ya que muchos predicados unarios se convirtieron en clases.

Smolka generalizó la lógica ordenada ordenada para permitir el polimorfismo paramétrico. En su marco, las declaraciones de subordenación se propagan a expresiones de tipos complejos. Como ejemplo de programación, se puede declarar una lista(X) de clasificación paramétrica (siendo X un parámetro de tipo como en una plantilla de C++), y de una declaración subsort int ⊆ float la relación list(int) ⊆ list(flotante) se infiere automáticamente, lo que significa que cada lista de enteros es también una lista de flotantes.

Schmidt-Schauß generalizó la lógica ordenada ordenada para permitir declaraciones de términos. Como ejemplo, suponiendo declaraciones de subclasificación par ⊆ int e odd ⊆ int, una declaración de término como ∀ i: int. (i + i): par permite declarar una propiedad de suma de enteros que no podría expresarse mediante sobrecarga ordinaria.

Unificación de términos infinitos

Antecedentes de árboles infinitos:

B. Courcelle (1983). "Fundamental Properties of Infinite Trees" (PDF). Teoreta. Comput. Sci. 25 (2): 95-169. doi:10.1016/0304-3975(83)90059-2. Archivado desde el original (PDF) on 2014-04-21. Retrieved 2013-06-28.
Michael J. Maher (Jul 1988). "Axiomatizaciones completas de los Álgebras de Árboles Finitos, Racionales e Infinitos". Proc. IEEE 3rd Annual Symp. on Logic in Computer Science, Edimburgo. págs. 348 a 357.
Joxan Jaffar; Peter J. Stuckey (1986). "Semántica de la programación lógica del árbol infinito". Theoretical Computer Science. 46: 141–158. doi:10.1016/0304-3975(86)90027-7.

Algoritmo de unificación, Prolog II:

A. Colmerauer (1982). K.L. Clark; S.-A. Tarnlund (eds.). Árboles Prolog e Infinitos. Prensa Académica.
Alain Colmerauer (1984). "Ecuaciones e Inequaciones sobre árboles finitos e infinitos". En ICOT (ed.). Proc. Int. Conf. on Fifth Generation Computer Systems. págs. 85 a 99.

Aplicaciones:

Francis Giannesini; Jacques Cohen (1984). "La generación más gruesa y la manipulación de gramática usando los árboles infinitos de Prolog". Journal of Logic Programming. 1 (3): 253–265. doi:10.1016/0743-1066(84)90013-X.

Unificación electrónica

E-unification es el problema de encontrar soluciones a un conjunto dado de ecuaciones, teniendo en cuenta algunos conocimientos básicos de ecuaciones E. Este último se da como un conjunto de igualdades universales. Para algunos conjuntos E particulares, 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 $x*adoteq y*b$ no tiene solución con respecto a la unificación puramente sintáctica, donde nada se sabe sobre el operador $*$ . Sin embargo, si el $*$ es conocido por ser conmutativo, entonces la sustitución ${} x \mapsto b, Sí. \mapsto a}$ resuelve la ecuación anterior, desde entonces

	$x*a$	${} x \mapsto b, Sí. \mapsto a}$
=	$b*a$		por solicitud de sustitución
=	$a*b$		por conmutación $*$
=	$y*b$	${} x \mapsto b, Sí. \mapsto a}$	por (converso) aplicación de sustitución

Los conocimientos de fondo E podría indicar la conmutación de $*$ por la igualdad universal " $u*v=v*u$ para todos $u, v$ ".

Conjuntos particulares de conocimientos previos E

**Convenciones de nombres usados**
$О u, v, w :$	${displaystyle u(vw)}$	=	${displaystyle (uv)w}$	$A$	Asociación de $*$
$О u, v :$	${displaystyle u*v}$	=	${displaystyle v*u}$	$C$	Computatividad de $*$
$О u, v, w :$	${displaystyle u*(v+w)}$	=	${displaystyle uv+uw}$	$D l$	Distribución de izquierdas $*$ sobre $+$
$О u, v, w :$	${displaystyle (v+w)*u}$	=	${displaystyle vu+wu}$	$D r$	Distribución correcta $*$ sobre $+$
$О u :$	${displaystyle u*u}$	=	$u$	$I$	Idempotencia $*$
$О u :$	${displaystyle n*u}$	=	$u$	$N l$	Elemento neutral izquierdo $n$ con respecto a $*$
$О u :$	${displaystyle u*n}$	=	$u$	$N r$	Elemento neutral derecho $n$ con respecto a $*$

Se dice que la unificación es decidible para una teoría, si se ha ideado un algoritmo de unificación para ella que termina 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 para ella que termina para cualquier problema de entrada soluble, pero puede seguir buscando para siempre soluciones de un problema de entrada irresoluble.

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

$A$
$A$ , $C$
$A$ , $C$ , $I$
$A$ , $C$ , $N l$
$A$ , $I$
$A$ , $N l$ $,$ $N r$ (monoide)
$C$
Anillos booleanos
Abelian groups, even if the signature is expanded by arbitrary additional symbols (but not axioms)
K4 álgebras modales

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

$A$ , $D l$ $,$ $D r$
$A$ , $C$ , $D l$
Anillos conmutativos

Paramodulación unilateral

Si hay un sistema de reescritura de términos convergentes R disponible para E, el algoritmo de paramodulación unilateral se puede utilizar para enumerar todas las soluciones de ecuaciones dadas.

Reglas de paramodulación unilaterales
G. f()s₁,...s_n≐ f()t₁,...t_n)	; S	⇒	G. s₁ ≐ t₁,... s_n ≐ t_n }	; S		decompose
G. x ≐ t }	; S	⇒	G {} x ↦ t }	; S{}x↦t.x↦t}	si la variable x no ocurre en t	eliminar
G. f()s₁,...s_n≐ t }	; S	⇒	G. s₁ u u₁,... s_n u u_n, r ≐ t }	; S	si f()u₁,...u_n) → r es una regla de R	mutate
G. f()s₁,...s_n≐ Sí. }	; S	⇒	G. s₁ ≐ Sí.₁,... s_n ≐ Sí._n, Sí. ≐ f()Sí.₁,...Sí._n)	; S	si Sí.₁,...Sí._n nuevas variables	imitar

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

Sistema de reescritura por término de ejemplo R
1	app()Nil,z)	→ z
2	app()x.Sí.,z)	→ x.app()Sí.,z)

Por ejemplo, se usa un sistema de reescritura de términos R para definir el operador agregar de listas construidas a partir de cons y nil; donde cons(x,y) se escribe en notación infija como x.y por brevedad; p.ej. aplicación(a.b.cero,c.d.cero) → a.aplicación(b.cero, c.d.nil) → a.b.aplicación (cero,c.d.cero) → 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 en los términos. Por ejemplo, aplicación(a.b.nil,c.d.cero) ≡ a.b.c.d.nil ≡ aplicación(a.b.c.d.cero,cero). El algoritmo de paramodulación enumera las soluciones de las ecuaciones con respecto a ese E cuando se alimenta con el ejemplo R.

Una ruta de cálculo de ejemplo exitosa 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 que las use la regla mutar; v₂, v₃,... 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 mutar, 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, aplicación(x,aplicación(y,x)) { y↦nil, x↦ a.nil } = aplicación(a.cero,aplicación(cero,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 satisfactoria, que se puede obtener seleccionando "mutar(1), mutar(2), mutar(2), mutar(1)" conduce a la sustitución S = { y ↦ a.a.nil, x ↦ nil }; no se muestra aquí. Ningún otro camino conduce al éxito.

Ejemplo de cálculo unificador
Regla de uso		G	S
		{} app()x,app()Sí.,x) ≐ a.a.Nil }	{}
mutate(2)	⇒	{} x ≐ v₂.v₃, app()Sí.,x≐ v₄, v₂.app()v₃,v₄≐ a.a.Nil }	{}
decompose	⇒	{} x ≐ v₂.v₃, app()Sí.,x≐ v₄, v₂ ≐ a, app()v₃,v₄≐ a.Nil }	{}
eliminar	⇒	{} app()Sí.,v₂.v₃≐ v₄, v₂ ≐ a, app()v₃,v₄≐ a.Nil }	{} x ↦ v₂.v₃ }
eliminar	⇒	{} app()Sí.,a.v₃≐ v₄, app()v₃,v₄≐ a.Nil }	{} x ↦ a.v₃ }
mutate(1)	⇒	{} Sí. ≐ Nil, a.v₃ ≐ v₅, v₅ ≐ v₄, app()v₃,v₄≐ a.Nil }	{} x ↦ a.v₃ }
eliminar	⇒	{} Sí. ≐ Nil, a.v₃ ≐ v₄, app()v₃,v₄≐ a.Nil }	{} x ↦ a.v₃ }
eliminar	⇒	{} a.v₃ ≐ v₄, app()v₃,v₄≐ a.Nil }	{} Sí. ↦ Nil, x ↦ a.v₃ }
mutate(1)	⇒	{} a.v₃ ≐ v₄, v₃ ≐ Nil, v₄ ≐ v₆, v₆ ≐ a.Nil }	{} Sí. ↦ Nil, x ↦ a.v₃ }
eliminar	⇒	{} a.v₃ ≐ v₄, v₃ ≐ Nil, v₄ ≐ a.Nil }	{} Sí. ↦ Nil, x ↦ a.v₃ }
eliminar	⇒	{} a.Nil ≐ v₄, v₄ ≐ a.Nil }	{} Sí. ↦ Nil, x ↦ a.Nil }
eliminar	⇒	{} a.Nil ≐ a.Nil }	{} Sí. ↦ Nil, x ↦ a.Nil }
decompose	⇒	{} a ≐ a, Nil ≐ Nil }	{} Sí. ↦ Nil, x ↦ a.Nil }
decompose	⇒	{} Nil ≐ Nil }	{} Sí. ↦ Nil, x ↦ a.Nil }
decompose	⇒	{}	{} Sí. ↦ Nil, x ↦ a.Nil }

Reducción

Diagrama Triángulo del paso de estrechamiento s ↝ t en posición p a plazo s, con sustitución unificadora σ (línea inferior), utilizando una regla de reescritura

l \to r

(top row)

Si R es un sistema de reescritura de términos convergente para E, un enfoque alternativo al apartado 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

la elección de un subtermo no variable del término actual,
sintactically unifying it with the left hand side of a rule from R, y
sustituir la mano derecha de la regla instantánea en el término instantáneo.

Formalmente, si $l \to 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$ se puede estrechar 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 se puede reducir a t se denota comúnmente como s ↝ t. Intuitivamente, una secuencia de pasos de estrechamiento t₁ ↝ t₂ ↝... ↝ t_n puede considerarse como una secuencia de pasos de reescritura t₁ → t₂ →... → t_n, pero con el término inicial t₁ siendo cada vez más instanciado, según sea necesario para que cada una de las reglas utilizadas sea aplicable.

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

app()

,app()Sí.,

)

↓

x ↦ v₂.v₃

app()

v₂.v₃

,app()Sí.,

v₂.v₃

)

→

v₂.app()v₃,app()

Sí.

,v₂.v₃)

↓

Sí. ↦ Nil

v₂.app()v₃,app()

Nil

,v₂.v₃)

→

v₂.app()

v₃

,v₂.

v₃

)

↓

v₃ ↦ Nil

v₂.app()

Nil

,v₂.

Nil

)

→

v₂.v₂.Nil

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

El lema restrictivo garantiza que cada vez 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 a un término $s'$ y $t'$ , respectivamente, tales que $t'$ es una instancia de $s'$ .

Formalmente: siempre que $sσ \to * t$ se cumple para alguna sustitución σ, entonces existen términos $s', t'$ tal que $s ↝ * s'$ y $t \to * t'$ y $s' τ = t'$ para alguna sustitución τ.

Unificación de orden superior

Muchas aplicaciones requieren que se considere la unificación de términos lambda escritos en lugar de términos de primer orden. Tal unificación a menudo se llama unificación de orden superior. La unificación de orden superior es indecidible, 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 el soluciones {f ↦ λx.λy.λz.d(y, x, c) }, {f ↦ λx.λ y.λz.d(y, z, c ) }, {f ↦ λx.λy.λz.d(y, a, c) }, {f ↦ λx.λy.λz.d(b, x, c) }, {f ↦ λx.λy.λz.d(b, z, c) } y {f ↦ λx.λy.λz.d(b, a, c) }. Una rama bien estudiada de la unificación de orden superior es el problema de unificar términos lambda simplemente tipificados módulo la igualdad determinada por conversiones αβη. Gérard Huet dio un algoritmo de (pre)unificación semidecidible que permite una búsqueda sistemática del espacio de unificadores (generalizando el algoritmo de unificación de Martelli-Montanari con reglas para términos que contienen variables de orden superior) que parece funcionar suficientemente bien en la práctica. Huet y Gilles Dowek 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. Unificación de patrones de orden superior, debida a Dale Miller, es otro subconjunto de este tipo. Los lenguajes de programación lógica de orden superior λProlog y Twelf han pasado de la unificación total 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 que no es de unificación de patrones 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. El demostrador del teorema de la posición de la cremallera tiene un algoritmo que integra estos subconjuntos de buen comportamiento en un algoritmo de unificación completo de orden superior.

En la 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 se determinan mediante la unificación de orden superior (HOU). Por ejemplo, la representación semántica de "A Jon le gusta Mary y a Peter también" es $like(j, m) \land R(p)$ y el valor de R (la representación semántica de los puntos suspensivos) está determinada por la ecuación $like(j, m) = R(j)$ . El proceso de resolución de tales ecuaciones se denomina unificación de orden superior.

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.

Contenido relacionado

Más resultados...