Programación funcional y lógica con restricciones

Resumen

En este trabajo presentamos e investigamos el esquema teórico cflp(x) para la programación lógico funcional perezosa con restricciones, cada estructura con restricciones x, que consiste en un dominio de Scott como soporte más un conjunto de operaciones predefinidas continuas, determina una instancia del esquema. Los programas en cflp(x) están constituidos por reglas de reescritura con restricciones para definir nuevas funciones. Se desarrolla una semántica declarativa de modelo mínimo, caracterizado también como mínimo punto fijo, y una semántica operacional basada en un mecanismo de cómputo - estrechamiento perezoso por restricciones - del que se prueban resultados de corrección y completitud con respecto a la semántica declarativa. Probamos también que, bajo hipótesis razonables, el estrechamiento por restricciones se puede combinar con un sistema de resolución de restricciones, preservando la corrección y la completitud. En una segunda parte se aplican los resultados obtenidos al lenguaje sfl, que incorpora restricciones de desigualdad a la programación lógico funcional perezosa. Se muestra que sfl puede ser concebido como la instancia de cflp(x) que tiene al universo de herbrand infinitario como soporte, dotado de restricciones de igualdad y desigualdad, mas las operaciones primitivas necesarias para expresar de forma continua la unificación. De este modo, hereda las propiedades generales del esquema. Finalmente se presenta, en forma de clausulas, una especificación de la semántica operacional, que se convierte en un programa prolog ejecutable al adoptar una adecuada representación de las expresiones, dando lugar a una implementación del lenguaje.