Resumen de Especificación orientada a objetos de sistemas de cálculo simbólico
- español
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.
- English
This work deals with the specification of symbolic computation systems in Algebraic Topology. In particular, two systems called EAT and Kenzo are studied. These programs obtain homology and homotopy groups of complex topological spaces, such as iterated loop spaces. These systems have provided groups that had never been obtained before by any other theoretical or mechanical method. From a computational point of view, these systems present the characteristic of having to build, at runtime, complex data structures that represent algebraic structures of infinite nature. This peculiarity makes their formal analysis particularly interesting.
This memoir is aimed at specifying these systems with three different approaches. The first approach involves redefining an operation among specifications, which was the basic notion of some previous works on the modelization of EAT data structures, using the institution's language (the notion of institution tries to formalize the concept of specification framework). Here, this operation is represented by a commutative diagram of institution morphisms, which allows to describe the operation in different specification frameworks like equational algebraic specification and some object-oriented formalisms, namely hidden specifications and the coalgebraic view. The second approach tries to extend the modelization to bigger fragments of EAT. In particular, operators representing functors among categories are specified. The last approach involves beginning the analysis of Kenzo data structures. To implement this system, in contrast to its predecessor EAT, object-oriented programming has been used, and therefore it has been necessary deal with techniques such as inheritance and polymorphism (at this point, the notion of coercion plays a key role).
The results obtained show that the data structures -and the relations among them- used in these systems form final objects in suitable categories of models. These results prove the "universal" nature of the codification chosen in the programs for these data structures and operations.
