Programación declarativa con restricciones sobre tipos de datos algebraicos

Résumé

El objetivo principal de esta tesis es introducir constructoras de datos algebraicas y restricciones dentro de la programación lógico funcional perezosa, Por constructoras de datos algebraicas entendemos constructoras de datos cuyo comportamiento está definido por un conjunto finito de axiomas ecuacionales. Presentamos un marco general para la programación lógico funcional perezosa que permite utilizar cualesquiera constructoras algebraicas gobernadas por axiomas ecuacionales fuertemente regulares (i.e., ambos lados de la ecuación contienen las mismas variables y un símbolo de constructora en cabeza), tipos polimórficos, igualdad estricta y funciones indeterministas. El marco resultante tiene una buena fundamentación teórica, tanto desde un punto de vista declarativo como operacional. Con respecto a la semántica declarativa, cualquier programa P, cuyas constructoras de datos estén gobernadas por un conjunto finito C de axiomas fuertemente regulares y bien tipificados, tiene modelos libres. Operacionalmente, hemos desarrollado un cálculo de resolución de objetivos que combina el estrechamiento perezoso con la unificación módulo las ecuaciones contenidas en C. El mecanismo operacional resultante es correcto y completo con respecto a la semántica declarativa. Como extensión natural del marco general (que sólo incorpora la restricción de igualdad) hemos investigado un lenguaje, denominado SETA, que permite manipular números reales, multiconjuntos (como única constructora algebraica), constructoras libres y restricciones. Más concretamente, SETA incorpora restricciones primitivas sobre números reales (al estilo del lenguaje CLP(R), de igualdad y desigualdad entre expresiones, y de pertenencia y no pertenencia de un elemento a un multiconjunto. Hemos demostrado que cualquier programa SETA tiene modelos libres gracias, en particular, a que el axioma de conmutatividad que rige el comportamiento de la constr