Funciones de orden superior en programación funcional: una perspectiva categórica

• Autores: José Enrique Freire Brañas
• Directores de la Tesis: José Luis Freire Nistal (1943-) (dir. tes.)
• Lectura: En la Universidade da Coruña ( España ) en 2003
• Idioma: español
• Número de páginas: 211
• Tribunal Calificador de la Tesis: Antonio Blanco Ferro (presid.) , Felicidad Aguado (secret.) , Eladio Domínguez Murillo (voc.) , Laureano Lambán Pardo (voc.) , Felipe Gago Couso (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • Identificación de las estructuras subyacentes a las categorías de Eilenberg-Moore y de Kleisli asociadas a las mónadas usadas en algunos lenguajes funcionales puros para modelizar aspectos imperativos.

    Dar una adecuada definición de la noción de tipo que permita abarcar estructuras abstractas.

    Definición de morfismos genéricos sobre esos tipos de forma que, aplicados a parámetros adecuados, posibiliten la construcción de programas funcionales verificables.

    Generalización de los teoremas de optimización (fusión y deforestación) aplicables a los morfismos previamente declarados.

    Implementación y optimización en CAML, usando los teoremas descritos en el apartado anterior, de los siguientes problemas: resolución, por medio de un algoritmo de búsqueda ciega, del problema PS de McCarthy, cálculo del número cromático y del spanning-tree de un grafo.

    Construcción de morfismos sobre tipos anidados con la posibilidad de ser singularizados analizando qué requerimientos son precisos para poder definir tales funciones.

    Caracterización de las funciones tail-recursive sobre los tipos regulares.

    Implementación y demostración en Coq de las propiedades previamente reseñadas.

    Definición en Coq de las funciones primitivo recursivas y de la noción de catamorfismo generalizado.

    Demostración en Coq del carácter catamórfico de la función de Ackermann.

    Demostración en Coq de la imposibilidad de declarar la función de Ackermann como catamorfismo generalizado.

    Caracterización de los cotipos según su carácter coninductivo analizando la equivalencia con su definición en Coq.