2009/08/31 by César Domínguez, César Dominguez, Dominguez, César +2
Computer Science · Mathematics · #Category Theory (math.CT) #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #cs.LO #math.CT
paper · pdf · doi:10.48550/arxiv.0908.4491
arxiv created 2009/08/31 · openalex publication_date 2009/08/31 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The parameterization process used in the symbolic computation systems Kenzo and EAT is studied here as a general construction in a categorical framework. This parameterization process starts from a given specification and builds a parameterized specification by adding a parameter as a new variable to some operations. 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. It is proved in this paper that the parameterization process is provided by a functor and the subsequent parameter passing process by a natural transformation. Various categorical notions are used, mainly adjoint functors, pushouts and lax colimits.