BOLETÍN ELECTRÓNICO CIENTÍFICO
DEL NODO BRASILERO
DE INVESTIGADORES COLOMBIANOS
Número 2(Artículo 19), 2000

TÍTULO
UNIFICACIóN DE ORDEN SUPERIOR VIA SUSTITUCIONES EXPLíCITAS

TIPO: Trabajo conjunto con F. Kamareddine realizado durante visita del autor al grupo ULTRA, CEE, Heriot-Watt University, Edimburgo, Escocia

AUTOR: Mauricio Ayala-Rincón ayala@mat.unb.br

IDIOMA: Inglés

DIRECCIÓN PARA CONTACTO

Departamento de Matemática, Universidade de Brasília, 70910-900 Brasília D. F., Brasil

ENTIDADES QUE FINANCIARON LA INVESTIGACIÓN: agencias Brasileras CAPES y FEMAT

PALABRAS CLAVE: Unificación de orden superior, teoría de tipos, teoría de reescritura, sustituciones explícitas

Introducción

A partir de la aparición del principio de resolución de Robinson [19], basado en sustitución, unificación y resolución, mucho trabajo ha sido realizado para formalizar estas nociones básicas en contextos más amplios. Tales extensiones son esenciales, entre otras cosas, para deducción automática en lógicas de orden superior.

La primera persona en formular exitosamente un método de unificación para el caso de lógicas de orden superior, más especificamente para el $ \lambda$-calculus tipado, fue Huet [9]. Desde entonces, diferentes concepciones de unificación de orden superior (HOU) han sido desarrolladas y utilizadas en lenguajes y demostradores de teoremas tales como el $ \lambda$prolog e Isabelle ([15,18]). En la mayoría de tales concepciones, la noción de sustitución juega un papel importante que ha llevado en años recientes a la producción de gran cantidad de trabajos para ``hacer la sustitución explícita''. También, mucho trabajo ha sido destinado a establecer la utilidad de las sustituciones explícitas en la deducción automática y la demostración de teoremas, síntesis de demostraciones [13,14], lenguajes de programación [4] y a la propia HOU [6]. El último trabajo muestra que sí la sustitución es hecha explícita se obtienen muchos beneficios en la computación de problemas de HOU. Particularmente, [6] presenta un método de unificación basado en el $ \lambda\sigma$-estilo de sustitución explícita, que en la práctica ha sido útil para deducción de problemas de HOU en el $ \lambda$-calculus tipado y subsecuentemente generalizado para el tratamiento de problemas de unificación ecuacional de orden superior [12] y restringido para el caso de patrones de orden superior [5].

Se desarrolló un método de HOU basado en el $ \lambda s_e$-estilo de sustitución explícita, que saca provecho de las cualidades del $ \lambda s_e$-calculus. En particular, esta concepción evita el uso de diferentes tipos de objetos como es necesario en el $ \lambda\sigma$-calculus. Adicionalmente, la decidibilidad de la aplicación de las reglas de unificación propuestas (i.e. determinación de los redices) depende de la busqueda de soluciones en los naturales de restricciones aritméticas simples. Todo esto hace $ \lambda s_e$-HOU más elegante y eficiente que $ \lambda\sigma$-HOU.

Unificación de orden superior

Objetos de orden superior aparecen naturalmente en muchos campos de la ciencia de la computación. Por ejemplo, en el contexto de implementación de lenguajes funcionales es necesario desarrollar mecanismos para el tratamiento de funciones de orden superior. Considere el siguiente sistema de reescritura que especifica la bien conocida función MAP, la cual aplica una función a todos los elementos de una lista: MAP$ (f,$NIL$ )\rightarrow$   NIL; MAP$ (f,$CONS$ (x, l))\rightarrow$   CONS$ (f(x),$MAP$ (f,l))$, donde $ \textsc{nil}$ y $ \textsc{cons}$ son las funciones usuales de LISP para la lista vacia y la constructora de listas, respectivamente. Observe que $ f$ aparece como una variable y como un símbolo de función. Desde el punto de vista de reescritura de primer orden, no es posible manipular este tipo de objetos. En efecto, para simples procesos deductivos basados en técnicas de reescritura, tales como un-paso de reducción o deducción de pares críticos, matching y unificación de primer orden no aplican. La solución para estos problemas, no sólo en el contexto de la reescritura, es el $ \lambda$-calculus.

MAP es un ejemplo típico de una función de segundo orden, pero funciones de tercer orden y de orden mayor son también de interés práctico. En [17] son presentadas funciones desde tercer hasta sexto orden de utilidad práctica computacional.

Un ejemplo simple de un problema de HOU es la busqueda de soluciones para la ecuación $ F(f(a)) = f(F(a))$ o equivalentemente $ ({({\lambda_{y}.{F}}\;\;{\lambda_{x}.{f}})}\;\;{a})= ({({\lambda_{x}.{f}}\;\;{\lambda_{y}.{F}})}\;\;{a})$. Una solución es la función identidad $ \{F/\lambda_{x}.{x}\}$, pero también son soluciones: $ \{F(x)/f^n(x)\;\vert\; n\in \mathbb{N}\}$.

El método de HOU de Huet [9] es importante porque él descubrió que para generalizar el principio de resolución de primer orden de Robinson a teorías de orden superior es útil verificar la existencia de unificadores sin necesidad de computarlos explícitamente. El procedimiento propuesto por Huet es de semi-decisión: puede nunca parar cuando el problema de entrada no tiene unificadores, pero cuando tiene una solución, parará presentando un unificador explícitamente. La unificación para la lógica de segundo orden fue demostrada indecidible en general por Goldfarb [8]. La demostración de Goldfarb es basada en una reducción para el décimo problema de Hilbert. Este resultado muestra que existen teorías arbitrarias de orden superior donde los problemas de unificación son indecidibles. Pero existen también lenguajes de orden superior particulares, de importancia práctica, donde los problemas de unificación son decidibles. Un caso especial de segundo orden, donde la unificación es decidible, es cuando el lenguaje es restringido a funciones monádicas [7].

Contribuciones del trabajo

El $ \lambda\sigma$-calculus [1] introduce dos conjuntos diferentes de entidades, una para términos y otra para sustituciones. El $ \lambda s_e$-calculus [11] se mantiene más cercano al $ \lambda$-calculus y utiliza la filosofía iniciada por de Bruijn en su sistema AUTOMATH [16] y elaborada extensivamente por medio de la notación de itens [10]. Tal filosofía establece que los términos del $ \lambda$-calculus son o bien términos de aplicación, tales como funciones aplicadas a un argumento; o términos de abstracción, tales como funciones; o términos de sustitución o actualización. De esta manera, sustitución y actualización son hechas explícitas en esta notación. Así, se estudió HOU en el $ \lambda s_e$-estilo de sustitución explícita desarrollando lo siguiente:

  1. Método correcto y completo de unificación en el $ \lambda s_e$-calculus;
  2. Método correcto y completo de transformación de problemas de HOU en el $ \lambda$-calculus en problemas de unificación en el lenguaje del $ \lambda s_e$-calculus;

Lo anterior permite reducir HOU a unificación de primer orden en el lenguaje del $ \lambda s_e$-calculus.

Adicionalmente, se comparó el método propuesto con el basado en el $ \lambda\sigma$-calculus llegando a la conclusión de que la utilización en $ \lambda s_e$-HOU de todos los índices de de Bruijn lo hace más eficiente, ya que en $ \lambda\sigma$-HOU unicamente es utilizado el índice $ \tt 1$ y los otros son simulados con operadores shift y composición de estos.

Finalmente aparece evidente que en $ \lambda s_e$-HOU la busqueda de redices es más simple que en $ \lambda\sigma$-HOU.

Algunos resultados del trabajo aqui divulgado aparecen en en [3,2].

Bibliografía

BECNBIC,2(19)2000