Especificación orientada a objetos de sistemas de cálculo simbólico

Resumen

El presente trabajo se centra en la especificación de sistemas de cálculo simbólico en Topología Algebraica. En particular, se estudian dos sistemas llamados EAT y Kenzo. Estos programas realizan cálculos de grupos de homología y de homotopía de espacios topológicos complejos, como por ejemplo espacios de lazos iterados. A través de ambos sistemas se han encontrado grupos que no han sido obtenidos por ningún otro método, ni teórico, ni automático. Desde el punto de vista de la computación estos sistemas presentan la característica de tener que construir, en tiempo de ejecución, estructuras de datos complejas que representan a estructuras algebraicas de naturaleza infinita. Esta peculiaridad hace interesante su análisis formal. La memoria plantea la tarea de especificación de estos sistemas por tres caminos diferentes. El primero consiste en redefinir una operación entre especificaciones, que es la pieza básica que se ha utilizado en trabajos previos para la modelización de las estructuras de datos de EAT, utilizando el lenguaje de las instituciones (la noción de institución pretende formalizar el concepto de marco de especificación). Se consigue representar dicha operación a través de un diagrama de morfismos de instituciones conmutativo, lo que permite describirla en distintos marcos de especificación como son la especificación algebraica ecuacional, y algunos formalismos orientados a objetos como la especificación oculta y el marco coalgebraico. El segundo camino pretende ampliar la modelización a fragmentos mayores de EAT. En particular se realiza la especificación de operadores que representan funtores entre categorías. El último camino supone el inicio del análisis de las estructuras de datos de Kenzo. Para implementar este sistema, a diferencia de su antecesor EAT, se ha utilizado programación orientada a objetos, por lo que ha sido necesario tratar la modelización de técnicas como la herencia y el polimorfismo (en este punto, la noción de coerción juega un papel fundamental). Se han obtenido resultados que muestran que las estructuras de datos, y las relaciones entre las mismas, que se utilizan en estos sistemas constituyen objetos finales en adecuadas categorías de modelos. Estos resultados vienen a demostrar el carácter "universal" de la codificación elegida en estos programas para estas estructuras de datos y operadores.