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

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 group...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Domínguez Pérez, César
Otros Autores: Lambán Pardo, Laureano (Universidad de La Rioja)
Formato: text (thesis)
Lenguaje:spa
Publicado: Universidad de La Rioja (España) 2003
Acceso en línea:https://dialnet.unirioja.es/servlet/oaites?codigo=75
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
id oai-TES0000000011
record_format dspace
institution DialNet
collection DialNet
language spa
description 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.
author2 Lambán Pardo, Laureano (Universidad de La Rioja)
author_facet Lambán Pardo, Laureano (Universidad de La Rioja)
Domínguez Pérez, César
format text (thesis)
author Domínguez Pérez, César
spellingShingle Domínguez Pérez, César
Especificación orientada a objetos de sistemas de cálculo simbólico
author_sort Domínguez Pérez, César
title Especificación orientada a objetos de sistemas de cálculo simbólico
title_short Especificación orientada a objetos de sistemas de cálculo simbólico
title_full Especificación orientada a objetos de sistemas de cálculo simbólico
title_fullStr Especificación orientada a objetos de sistemas de cálculo simbólico
title_full_unstemmed Especificación orientada a objetos de sistemas de cálculo simbólico
title_sort especificación orientada a objetos de sistemas de cálculo simbólico
publisher Universidad de La Rioja (España)
publishDate 2003
url https://dialnet.unirioja.es/servlet/oaites?codigo=75
work_keys_str_mv AT dominguezperezcesar especificacionorientadaaobjetosdesistemasdecalculosimbolico
_version_ 1718346546355896320
spelling oai-TES00000000112016-04-13Especificación orientada a objetos de sistemas de cálculo simbólicoDomínguez Pérez, CésarThis 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.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.Universidad de La Rioja (España)Lambán Pardo, Laureano (Universidad de La Rioja)Rubio García, Julio (Universidad de La Rioja)2003text (thesis)application/pdfhttps://dialnet.unirioja.es/servlet/oaites?codigo=75(Tesis) ISBN 84-688-2365-1 spaLICENCIA DE USO: Los documentos a texto completo incluidos en Dialnet son de acceso libre y propiedad de sus autores y/o editores. Por tanto, cualquier acto de reproducción, distribución, comunicación pública y/o transformación total o parcial requiere el consentimiento expreso y escrito de aquéllos. Cualquier enlace al texto completo de estos documentos deberá hacerse a través de la URL oficial de éstos en Dialnet. Más información: https://dialnet.unirioja.es/info/derechosOAI | INTELLECTUAL PROPERTY RIGHTS STATEMENT: Full text documents hosted by Dialnet are protected by copyright and/or related rights. This digital object is accessible without charge, but its use is subject to the licensing conditions set by its authors or editors. Unless expressly stated otherwise in the licensing conditions, you are free to linking, browsing, printing and making a copy for your own personal purposes. All other acts of reproduction and communication to the public are subject to the licensing conditions expressed by editors and authors and require consent from them. Any link to this document should be made using its official URL in Dialnet. More info: https://dialnet.unirioja.es/info/derechosOAI