Strategies and analysis techniques for functional program optimization

Resumen

Los sistemas informáticos desempeñan un papel importante en la moderna sociedad de la información. Sin embargo, la baja calidad del software y su bajo nivel de abstracción inhiben la necesaria confianza de los usuarios finales y desarrolladores de sistemas en la ingeniería de la programación. La corrección de programas informáticos a través de una teoría matemática de la computación es el primordial interés de la teoría de la programación y de su aplicación a la ingeniería de la programación a gran escala. Los métodos formales proveen a la ingeniería de la programación del adecuado marco científico y tecnológico para convertirse en una ingeniería real, tan predecible como son la ingeniería de caminos, canales y puertos o la ingeniería industrial. De hecho, el uso durante todas las etapas del desarrollo de programas, de lenguajes de programación declarativos basados en reglas, asegura la utilización de metodologías formales correctas y certificadas a lo largo del proceso de producción de programas. Los programas se describen normalmente como sistemas de reescritura de términos en los lenguajes de programación declarativos basados en reglas. La ejecución de un programa consiste en reducir (o reescribir) términos de entrada en términos de salida con la aplicación de una secuencia de reglas. El estrechamiento es una extensión de la reescritura para sistemas de reescritura de términos que permite la instanciación de variables en los términos de entrada con el objetivo de activar pasos de reescritura en la expresión instanciada. La reescritura (así como el estrechamiento) son en general indecidibles, es decir no se puede determinar si un término se reescribe (o estrecha) a otro. El espacio de reducción asociado a un término de entrada es enorme debido a las diferentes posibilidades de selección de los subtérminos a reducir y las reglas aplicables a dichos subtérminos. Esta situación se agrava en el caso del estrechamiento debido al proceso de instanciación. Esta tesis afronta el problema de cómo definir métodos eficientes para mejorar el comportamiento computacional de los sistemas de reescritura de términos, es decir, restringir el espacio de reducción asociado a un término de entrada selecionando qué términos y/o reglas serán usados por la reescritura (o el estrechamiento).