- 【Updated on May 12, 2025】 Integration of CiNii Dissertations and CiNii Books into CiNii Research
- Trial version of CiNii Research Knowledge Graph Search feature is available on CiNii Labs
- 【Updated on June 30, 2025】Suspension and deletion of data provided by Nikkei BP
- Regarding the recording of “Research Data” and “Evidence Data”
Parameterizations and Fixed-Point Operators on Control Categories
Description
The λμ-calculus features both variables and names together with their binding mechanisms. This means that constructions on open terms are necessarily parameterized in two different ways for both variables and names. Semantically, such a construction must be modeled by a biparameterized family of operators. In this paper, we study these biparameterized operators on Selinger's categorical models of the λμ-calculus called control categories. The overall development is analogous to that of Lambek's functional completeness of cartesian closed categories via polynomial categories. As a particular and important application of such consideration, we study the parameterizations of uniform fixed-point operators on control categories. We show a bijective correspondence between biparameterized fixed-point operators and nonparameterized ones under the uniformity conditions.