Programación declarativa con restricciones sobre tipos de datos algebraicos

  1. Arenas Sánchez, Purificación
Dirigida por:
  1. Mario Rodríguez Artalejo Director

Universidad de defensa: Universidad Complutense de Madrid

Año de defensa: 1999

Tribunal:
  1. David de Frutos Escrig Presidente
  2. Narciso Martí Oliet Secretario
  3. María Alpuente Frasnedo Vocal
  4. Giorgio Levi Vocal
  5. Ernesto Pimentel Sánchez Vocal

Tipo: Tesis

Teseo: 70506 DIALNET

Resumen

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