Análisis semántico y transformación de programas lógico-funcionales

Abstract

El problema de la integraci on de la programaci on l ogica y funcional est a considerado como uno de los m as importantes en el area de investigaci on sobre programaci on declarativa. Para que los lenguajes declarativos sean utiles y puedan utilizarse en aplicaciones reales, es necesario que el grado de e ciencia de su ejecuci on se aproxime al de los lenguajes imperativos, tal y como se ha conseguido con el lenguaje Prolog. Para ello, es imprescindible el desarrollo de herramientas potentes para el an alisis y transformaci on de los programas, capaces de optimizar las implementaciones realizadas. En general, es deseable sustituir las aproximaciones ad-hoc por tratamientos m as sistem aticos para los problemas de an alisis y transformaci on de programas. Puesto que la sem antica de los lenguajes l ogico{funcionales ha sido objeto de numerosos estudios y est a matem aticamente bien formalizada, surge el inter es por el desarrollo de m etodos y t ecnicas formales para la formulaci on de optimizaciones, basadas en la sem antica, que preserven las propiedades computacionales del programa. Esta tesis se centra en el desarrollo de tales t ecnicas, adopt andose una aproximaci on formal basada en la sem antica (operacional) del lenguaje para desarrollar y analizar, en un contexto uni cado, las diferentes optimizaciones. En la primera parte, desarrollamos un marco para el an alisis est atico de programas l ogico{funcionales, basado en la idea de construir aproximaciones correctas de la sem antica operacional del programa. Formalizamos un esquema de an alisis simple, uniforme y exible, que permite estudiar distintos tipos de propiedades (relacionadas con el conjunto de respuestas computadas por el programa) de manera correcta y f acilmente implementable. El esquema es independiente de la estrategia de narrowing usada en la formulaci on del mecanismo operacional del lenguaje, lo que contribuye a dar generalidad al mismo. Las t ecnicas de evaluaci on parcial son, de entre la gran variedad de t ecnicas existentes para la transformaci on de programas, las que mayor inter es han despertado en las dos ultimas d ecadas. Su utilidad no reside unicamente en la posibilidad de especializar programas, sino que sus aplicaciones se extienden tambi en a la generaci on autom atica de compiladores o a la optimizaci on de c odigo, por citar s olo las m as importantes. En la segunda parte de esta tesis mostramos que, en el contexto de los len- i guajes l ogico{funcionales, la especializaci on de programas se puede basar directamente en el mecanismo operacional de narrowing que, debido a la propagaci on bidireccional de par ametros realizada a trav es del procedimiento de uni caci on, es capaz de producir optimizaciones apreciables. Esta visi on uni cada de ejecuci on y especializaci on nos permite explotar las contribuciones de ambos campos, funcional y l ogico, y desarrollar un esquema simple y potente para mejorar el programa original respecto a su capacidad para computar respuestas. Tambi en mostramos que, debido a la componente funcional, son posibles otras optimizaciones (como la inclusi on de pasos de simpli - caci on deterministas) con el bene cio a~nadido de que, en nuestro esquema, todas las optimizaciones quedan `compiladas' en el programa transformado. Formalizamos los conceptos b asicos para la evaluaci on parcial de programas l ogico{funcionales y demostramos la correcci on y completitud de la transformaci on. El esquema presentado en este trabajo constituye la primera aproximaci on totalmente autom atica, correcta y nita para la evaluaci on parcial de programas l ogico{funcionales.