Programación lógico-funcional con tipos paramétricos y géneros ordenados

Resumen

Presentamos un lenguaje lógico-funcional con subtipos en el que las reglas de programa consisten en reglas de reescritura bien tipificadas condicionales basadas en constructoras donde las condiciones pueden contener ecuaciones y condiciones de tipos, Para este lenguaje damos diferentes caracterizaciones semánticas, primero mediante una lógica de reescritura tipificada, que permite probar la validez ecuaciones y condiciones de tipos respecto a un programa. Unido a este, definimos una semántica operacional basada en estrechamiento perezoso y que combina la unificación perezosa con la resolución de ecuaciones, la comprobación de tipos para expresiones y la resolución de subtipos y probamos que la semántica operacional es correcta y completa respecto a la lógica de reescritura. Por otro lado, estudiamos la semántica denotacional y declarativa del lenguaje, a través del estudio de los modelos de Scott de un programa. Probamos que existe un modelo libremente generado en la categoría de modelos de un programa que es punto fijo de un operador de consecuencias inmediatas definido a partir del programa, y probamos que la semántica denotacional es correcta y completa con respecto a la lógica de reescritura. Además describimos la implementación del lenguaje basada en traducir los programas a Prolog, en la que se describe como el uso de los tipos permite la poda del espacio de búsqueda de soluciones de un objetivo. Como parte de la implementación, estudiamos el análisis de tipos en tiempo de compilación, proporcionando mecanismos de inferencia y comprobación de tipos. Finalmente estudiamos cómo extender el lenguaje con funciones de orden superior.