Parameterizations and Fixed-Point Operators on Control Categories

Issue title: Typed Lambda Calculi and Applications 2003, Selected Papers

Article type: Research Article

Authors: Kakutani, Yoshihiko | Hasegawa, Masahito

Affiliations: Department of Information Science, University of Tokyo. kakutani@is.s.u-tokyo.ac.jp | Research Institute for Mathematical Sciences, Kyoto University, PRESTO, Japan Science and Technology Agency. hassei@kurims.kyoto-u.ac.jp

Note: [] Address for correspondence: Department of Information Science, University of Tokyo

Abstract: 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.

Journal: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 153-172, 2005