作为范畴构造的参数化过程
A parameterization process as a categorical construction
摘要：
本文研究了符号计算系统Kenzo和EAT中的参数化过程，并将其作为范畴框架中的一般构造。这个参数化过程从给定的规范开始，通过将一些操作转换为参数化操作来构建参数化规范，这些操作依赖于一个称为参数的附加变量。给定一个参数化规格说明的模型，对参数的每个解释（称为参数）都提供了给定规格说明的模型。此外，在某些相关的终结性假设下，给定规格说明的参数和模型之间的这种对应关系是双射。本文证明了参数化过程是由一个自由函子提供的，而随后的参数传递过程是由一个自然变换提供的。使用了各种范畴概念，主要是伴随函子，推出和松弛余极限。
英文摘要：
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 transforming some operations into parameterized operations, which depend on one additional variable called the parameter. 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 free functor and the subsequent parameter passing process by a natural transformation. Various categorical notions are used, mainly adjoint functors, pushouts and lax colimits.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
