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

En la primera parte de este trabajo proponemos un nuevo marco teorico que permite caracterizar la semantica declarativa y operacional de los lenguajes de programacion logico funcionales perezosos con restricciones, a traves del desarrollo de un esque ma generico CFLP(D) sobre un dominio D parametricamente dado, Sobre la base de una nueva formalizacion matematica de este dominio y de su resolutor asociado, el nuevo esquema permite definir instancias particulares de interes practico, como el domini o de Herbrand H, el dominio R de los numeros reales, o el dominio FD de los numeros enteros con restricciones de dominio finito, para los que el esquema proporciona ademas lenguajes concretos de programacion mediante programas constituidos por reglas de reescritura con restricciones que definen nuevas funciones. El esquema CFLP(D) permite caracterizar la semantica declarativa de este tipo de programas a partir de una nocion adecuada de c-interpretacion sobre un dominio, gracias a la cual se def inen dos clases de semanticas de modelos, denominadas, respectivamente, semantica debil y semantica fuerte. Demostramos la existencia de un modelo minimo para cada una de estas dos semanticas, caracterizandolo como minimo punto fijo. El desarrollo de una logica de reescritura con restricciones denominada CRWL(D), tambien definida de forma parametrica sobre un dominio de restricciones D arbitrario, permite proporcionar un nuevo marco logico para la programacion en el esquema CFLP(D), y en consecu encia, una forma alternativa muy util de caracterizar la semantica declarativa de los programas. Con el fin de proporcionar tambien una base formal a la semantica operacional del esquema CFLP(D), proponemos dos metodos de resolucion de objetivos par a programas que hacen uso del estrechamiento como mecanismo de computo. En primer lugar, se presenta un calculo de transformacion de objetivos denominado CLNC(D), basado en estrechamiento perezoso con restricciones, para el que demostramos su correcc ion y completitud fuerte con respecto a la semantica declarativa de CRWL(D). En segundo lugar, introducimos un refinamiento eficiente mediante el calculo CDNC(D) que permite integrar arboles definicionales con el proposito de asegurar que todos los p asos que se ejecutan en los computos son realmente necesarios. Como aplicacion practica, describimos el sistema TOY(FD), una implementacion de la instancia particular CFLP(FD) en el sistema logico funcional con restricciones TOY. En la segunda parte