A parameterization process: from a functorial point of view (Q2909193)

From the Introduction: ``Kenzo and its predecessor EAT are software systems devoted to symbolic computation in algebraic topology. They carry out calculations of homology groups of complex topological spaces, namely iterated loop spaces.NEWLINENEWLINEThis paper deals with generalization by parameterization in the sense of Kenzo and EAT, so that our parameters are symbolic constants of a given type, that will be replaced by arguments which are elements in a given set. The notion of parameterization in programming and specification languages bears several meanings, where the parameter may be a type or a specification. For instance, in object oriented programming, parametric polymorphism is called generic programming, in C++ it is characterized by the use of template parameters to represent abstract data types. On the other hand, in algebraic specifications, a parameterized specification is defined as a morphism of specifications where the parameter is the source and the parameter passing is defined as a pushout [\textit{H. Ehrig} et al., Lect. Notes Comput. Sci. 85, 157--168 (1980; Zbl 0456.68101)].NEWLINENEWLINEA theory \(\Theta\) can be presented by a specification \(\Sigma\), this means that \(\Sigma\) generates \(\Theta\).NEWLINENEWLINEThe parameterization process and its associated parameter passing process have been described for each given theory \(\Theta\), but in fact they have the property of preserving the theory structure, which can be stated precisely in a categorical framework: this is the aim of this paper.''NEWLINENEWLINEThe authors also prove the following: ``Given a model of the parameterized specification, each interpretation of the parameter, called an argument, provides a model of the given specification. Moreover, under some relevant terminality assumption, this correspondence between the arguments and the models of the given specification is a bijection.''