Parameterizations and fixed-point operators on control categories
Yoshihiko Kakutani and Masahito Hasegawa
In
Proc. 6th
International Conference on Typed Lambda Calculi and Applications
(TLCA'03),
Springer LNCS
2701 (2003) pages 180-194
Abstract
The \lambda\mu-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 bi-parameterized family of operators. In this paper, we study
these bi-parameterized operators on Selinger's categorical models of
the \lambda\mu-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 case, we study parameterizations of uniform
fixed-point operators on control categories, and show bijective
correspondences between parameterized fixed-point operators and
non-parameterized ones under uniformity conditions.
© Springer-Verlag 2003
Pointers to Related Work
- Y. Kakutani,
Duality between call-by-name recursion and call-by-value iteration.
In Proc. Computer Science Logic, Springer LNCS 2471 (2002) pp. 506-521.
- P.
Selinger,
Control categories and duality: on the categorical semantics of
the lambda-mu calculus.
Math. Structures Comput. Sci. 11(2) (2001) 207-260.
Back to Hassei's
Research Page / Home Page