Un esquema de programación lógico-funcional con restriccionesmarco teórico y aplicación a la depuración declarativa

Resumen

En la primera parte de este trabajo proponemos un nuevo marco teórico que permite caracterizar la semántica declarativa y operacional de los lenguajes de programación lógico funcionales perezosos con restricciones, a través del desarrollo de un esque ma genérico CFLP(D) sobre un dominio D paramétricamente dado, Sobre la base de una nueva formalización matemática de este dominio y de su resolutor asociado, el nuevo esquema permite definir instancias particulares de interés práctico, como el domini o de Herbrand H, el dominio R de los números reales, o el dominio FD de los números enteros con restricciones de dominio finito, para los que el esquema proporciona además lenguajes concretos de programación mediante programas constituidos por reglas de reescritura con restricciones que definen nuevas funciones. El esquema CFLP(D) permite caracterizar la semántica declarativa de este tipo de programas a partir de una noción adecuada de c-interpretación sobre un dominio, gracias a la cual se def inen dos clases de semánticas de modelos, denominadas, respectivamente, semántica débil y semántica fuerte. Demostramos la existencia de un modelo mínimo para cada una de estas dos semánticas, caracterizándolo como mínimo punto fijo. El desarrollo de una lógica de reescritura con restricciones denominada CRWL(D), también definida de forma paramétrica sobre un dominio de restricciones D arbitrario, permite proporcionar un nuevo marco lógico para la programación en el esquema CFLP(D), y en consecu encia, una forma alternativa muy útil de caracterizar la semántica declarativa de los programas. Con el fin de proporcionar también una base formal a la semántica operacional del esquema CFLP(D), proponemos dos métodos de resolución de objetivos par a programas que hacen uso del estrechamiento como mecanismo de cómputo. En primer lugar, se presenta un cálculo de transformación de objetivos denominado CLNC(D), basado en estrechamiento perezoso con restricciones, para el que demostramos su correcc ión y completitud fuerte con respecto a la semántica declarativa de CRWL(D). En segundo lugar, introducimos un refinamiento eficiente mediante el cálculo CDNC(D) que permite integrar árboles definicionales con el propósito de asegurar que todos los p asos que se ejecutan en los cómputos son realmente necesarios. Como aplicación práctica, describimos el sistema TOY(FD), una implementación de la instancia particular CFLP(FD) en el sistema lógico funcional con restricciones TOY. En la segunda parte