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 bi-parameterized family of operators. In this paper, we study these bi-parameterized 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 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
S. Bloom and Z. Ésik. Iteration Theories. EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1993.
C. Führmann. Varieties of effects. In Foundations of Software Science and Computation Structures, volume 2303 of LNCS, pages 144–158, Springer-Verlag, 2002.
M. Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec. PhD thesis, University of Edinburgh, 1997.
M. Hasegawa and Y. Kakutani. Axioms for recursion in call-by-value. Higher-Order and Symbolic Computation, 15(2):235–264, 2002.
B. Jacobs. Parameters and parameterization in specification, using distributive categories. Fundamenta Informaticae, 24(3):209–250, 1995.
Y. Kakutani. Duality between call-by-name recursion and call-by-value iteration. In Computer Science Logic, volume 2471 of LNCS, pages 506–521, Springer-Verlag, 2002.
J. Lambek. Functional completeness of cartesian categories. Annals of Mathematical Logic, 6:259–292, 1970.
J. Lambek and P.J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1986.
M. Parigot. λµ-calculus: an algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, volume 624 of LNCS, pages 190–201, Springer-Verlag, 1992.
A.J. Power and E.P. Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7(5):453–468, 1997.
P. Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science, 11(2):207–260, 2001.
A. Simpson and G. Plotkin. Complete axioms for categorical fixed-point operators. In Proceedings of 15th Annual Symposium on Logic in Computer Science, pages 30–41, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kakutani, Y., Hasegawa, M. (2003). Parameterizations and Fixed-Point Operators on Control Categories. In: Hofmann, M. (eds) Typed Lambda Calculi and Applications. TLCA 2003. Lecture Notes in Computer Science, vol 2701. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44904-3_13
Download citation
DOI: https://doi.org/10.1007/3-540-44904-3_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40332-6
Online ISBN: 978-3-540-44904-1
eBook Packages: Springer Book Archive