Resumen de Objetos localmente efectivos y tipos abstractos de datos

María Vico Pascual Martínez-Losa

• español

  Existen muchas técnicas que permiten abordar, parcialmente, uno de los problemas centrales en Informática Aplicada: el problema de verificar si un programa funciona correctamente, es decir, si funciona como los usuarios esperan de él. En esta tesis se realizan aportaciones en el análisis de los tipos de datos manipulados por los programas. Concretamente, el trabajo se centra en modelar las estructuras de datos que aparecen en un sistema de Cálculo Simbólico denominado EAT (Effective Algebraic Topology) diseñado por Rubio y Sergeraert. EAT es un sistema escrito en Common Lisp y dedicado a realizar cálculos en Topología Algebraica. Ha resultado ser útil para calcular grupos de homología de espacios topológicos infinitos (en concreto, espacios de lazos iterados). Para realizar el análisis formal de las estructuras de datos del sistema EAT, se define una operación entre Tipos Abstractos de Datos (en el marco clásico de Especificación Algebraica?, inspirada por la forma en la que EAT trabajo con estructuras matemáticas complejas.

  Al buscar relaciones con los tópicos actuales en el campo de Especificación Algebraica, encontramos que nuestra aproximación está muy relacionada con algunos formalismos orientados a objeto, concretamente con las especificaciones ocultas y el marco coalgebraico. Estas relaciones hacen explícitas las características orientadas a objeto implícitas del sistema EAT.

  La principal herramienta utilizada es una operación sintáctica entre signaturas, denotada ()imp, que se extiende a Tipos Abstractos de Datos y que pretende recoger la forma de trabajar de EAT. Esta operación construye, a partir de un tipo abstracto de datos T, un nuevo tipo abstracto de datos, Timp, que debería considerarse como el tipo abstracto de datos de las implementaciones de T. Además, establecemos un marco de implementación en el que probamos que las estructuras de datos utilizadas en EAT son implementaciones de tipos abstractos de datos Timp. En este marco se obtienen resultados matemáticos que caracterizan a las estructuras de datos de EAT como coproductos y objetos finales en ciertas categorías de implementaciones, lo que nos permite afirmar que la forma de implementación de EAT posee las propiedades adecuadas. Esta caracterización recoge tanto a las estructuras de datos que codifican estructuras algebraicas de naturaleza finita, denominadas Objetos Efectivos, como a las que codifican información de naturaleza infinita, denominadas Objetos Localmente Efectivos.

• English

  There are a lot of techniques that allow to tackle the problem of verifying whether a program runs correctly, that is, in the way intended by the user.

  This doctoral thesis represents a contribution to the analysis of the data types handled by programs. Particularly, we focused on the modelling of data structures in a Symbolic Computation system called EAT (Effective Algebraic Topology) designed by Rubio and Sergeraert. EAT is a Common Lisp system devoted to Algebraic Topology and a tool for the mechanized computation of homology groups of infinite topological spaces (namely, iterated loop spaces). In order to perform a formal analysis of the EAT data structures, an operation on Abstract Data Types is defined. This operation (defined within the classical Algebraic Specification framework) is inspired by the EAT way of working with complex mathematical structures. Looking for a connection with the current mainstream topics in the field of Algebraic Specification, we found that our approach was closely related to some object-oriented formalisms, namely, hidden specifications and the coalgebraic view. These relations made explicit the implicit object-oriented features of the EAT system. This was unexpected since the crux in EAT is the role of the functional programming.

  The main tool used is a syntactic operation between signatures, denoted ()imp, which is extended to Abstract Data Types and intends to capture the EAT way of working. This operation constructs from an abstract data type T a new abstract data type, Timp, which should be considered as the abstract data type of the implementations of T. We established an implementation framework in which we proved that the EAT data structures used are implementations of Timp abstract data types. Moreover, we obtained mathematical results that characterize the EAT data structures as coproducts and final objects in certain categories of implementations. These results allow us to claim that the EAT way of implementation has appropriate properties.

  The characterization of the EAT data structures obtained includes those coding algebraic structures of finite nature, called Effective Objects, as well as those coding information of infinite nature, called Locally Effective Objects.