Parameterizations and Fixed-Point Operators on Control Categories

• Autorzy: Kakutani Y. , Hasegawa M.
• Języki publikacji: EN

Abstrakty

EN

The lm-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 lm-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.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 65, nr 1,2
• Strony: 153--172
• Opis fizyczny: Bibliogr. 16 poz.

Twórcy

autor

Kakutani Y.

• Department of Information Science, University of Tokyo

autor

Hasegawa M.

• Research Institute for Mathematical Sciences, Kyoto University PRESTO, Japan Science and Technology Agency

Bibliografia

• [1] Bloom, S., Ėsik, Z.: Iteration Theories, EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1993.
• [2] Fiore, M.: Axiomatic Domain Theory in Categories of Partial Maps, Distinguished Dissertation Series, Cambridge University Press, 1996.
• [3] Führmann, C.: Varieties of Effects, in: Foundations of Software Science and Computation Structures, vol. 2303 of LNCS, Springer-Verlag, 2002, 144–158.
• [4] Hasegawa, M.: Models of Sharing Graphs: a categorical semantics of let and letrec, Ph.D. Thesis, University of Edinburgh, 1997, Also available as Distinguished Dissertation Series, Springer-Verlag, 1999.
• [5] Hasegawa, M., Kakutani, Y.: Axioms for Recursion in Call-by-Value, Higher-Order and Symbolic Computation, 15(2), 2002, 235–264.
• [6] Jacobs, B.: Parameters and Parameterization in Specification, Using Distributive Categories, Fundamenta Informaticae, 24(3), 1995, 209–250.
• [7] Kakutani, Y.: Duality between Call-by-Name Recursion and Call-by-Value Iteration, in: Computer Science Logic, vol. 2471 of LNCS, Springer-Verlag, 2002, 506–521.
• [8] Lambek, J.: Functional Completeness of Cartesian Categories, Annals of Mathemathical Logic, 6, 1970, 259–292.
• [9] Lambek, J., Scott, P. J.: Introduction to Higher-Order Categorical Logic, Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1986.
• [10] Laurent, O.: Polarized Proof Nets and __-calculus, Theoretical Computer Science, 290(1), 2002, 161–188.
• [11] Montelatici, R.: Polarized Proof Nets with Cycles and Fixpoints Semantics, in: Typed Lambda Calculi and Applications, vol. 2701 of LNCS, Springer-Verlag, 2003, 256–270.
• [12] Parigot, M.: λμ-calculus: an algorithmic interpretation of classical natural deduction., in: Logic Programming and Automated Reasoning, vol. 624 of LNCS, Springer-Verlag, 1992, 190–201.
• [13] Power, A. J., Robinson, E. P.: Premonoidal Categories and Notions of Computation, Mathematical Structures in Computer Science, 7(5), 1997, 453–468.
• [14] Selinger, P.: Control Categories and Duality: on the categorical semantics of the lambda-mu calculus, Mathematical Structures in Computer Science, 11(2), 2001, 207–260.
• [15] Simpson, A., Plotkin, G.: Complete Axioms for Categorical Fixed-point Operators, in: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 2000, 30–41.
• [16] Thielecke, H.: Categorical Structure of Continuation Passing Style, Ph.D. Thesis, University of Edinburgh, 1997.