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

Abstract

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.