Category Theoretic Semantics for Typed Binding Signatures with Recursion

• Autorzy: Power J. , Tanaka M.
• Języki publikacji: EN

Abstrakty

EN

We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do this in an enriched setting, allowing the incorporation of recursion into the analysis. Extending earlier work by us, we axiomatise the notion of context by defining and using the notion of an enriched pseudo-monad S on V-Cat, with leading examples of V given by Set and wCpo, the latter yielding an account of recursion. Fiore et al implicitly used the pseudo-monad Tfp on Cat for small categories with finite products. Given a set A of types, our extension to typed binders and enrichment involves generalising from Fiore et al's use of [\mathbbF,Set] to [(SA)op,VA]. We define a substitution monoidal structure on [(SA)op,VA], allowing us to give a definition of binding signature at this level of generality, and extend initial algebra semantics to the typed, enriched axiomatic setting. This generalises and axiomatises previous work by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, infinitary examples, and structures not previously considered such as those generated by finite limits.

Słowa kluczowe

EN

pseudo-monad; pseudo-distributive law; binding; substitution monoidal structure; binding signature

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 84, nr 2
• Strony: 221--240
• Opis fizyczny: bibliogr. 32 poz.

Twórcy

autor

Power J.

autor

Tanaka M.

• School of Informatics, University of Edinburgh, King's Buildings, Edionburgh EH9 3JZ, Scotland,

Bibliografia

• [1] S. J. Ambler, R. L. Crole, and Alberto Momigliano. A Definitional Approach to Primitive Recursion over Higher Order Abstract Syntax. In Proc. MERLIN 2003, ACM Digital Library, 2003.
• [2] Gian Luca Cattani and Glynn Winskel. Profunctors, Open Maps and Bisimulation. Mathematical Structures in Computer Science 15: 553-614, 2005.
• [3] James Cheney. Toward a General Theory of Names, Binding and Scope. In Proc. MERLIN 2005, ACM Digital Library, 2005.
• [4] S. Eilenberg and G. M. Kelly. Closed categories. In Proc. Conf. on Categorical Algebra (La Jolla, 1965), pages 421-562, 1966.
• [5] M. Fiore, Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proc. PPDP 02, ACM Press, pages 26-37, 2002.
• [6] M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. LICS 99, pages 193-202. IEEE Press, 1999.
• [7] M. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13:341-363, 2002.
• [8] M. Hofmann, Semantical analysis of higher-order abstract syntax. In Proc. LICS 99, IEEE Press, pages 204-213, 1999.
• [9] M. Hyland and A. J. Power. Pseudo-commutativemonads and pseudo-closed 2-categories. J. Pure and Applied Algebra 175:141-185, 2002.
• [10] B. Jacobs. Categorical Logic and Type Theory. Elsevier, 1999.
• [11] G. B. Im and G. M. Kelly. A universal property of the convolution monoidal structure. J. Pure Appl. Algebra 43:75-88, 1986.
• [12] G. M. Kelly. An abstract approach to coherence. In Coherence in categories, LNM 281, pages 106-147, 1972. 181-256,
• [13] G. M. Kelly. Basic Concepts of Enriched Category Theory, London Math. Soc. Lecture Notes Series 64 Cambridge University Press, 1982.
• [14] G. M. Kelly. Structures defined by finite limits in the enriched context I. Cahiers de Topologie et Géométrie Diffé rentielle 23:3-42, 1982.
• [15] G. M. Kelly and A. J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. J. Pure Appl. Algebra 89:163-179, 1993.
• [16] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.
• [17] M. Miculan and I. Scagnetto. A framework for typed HOAS and semantics. In Proc. PPDP 2003, ACM Press, pages 184-194, 2003.
• [18] P. O'Hearn. On Bunched Typing, Journal of functional Programming 13:747-796, 2003.
• [19] P. W. O'Hearn and R. D. Tennent. Relational parametricity and local variables. In Proc. 20th POPL, ACM Press, 1993.
• [20] P. W. O'Hearn and R. D. Tennent. Algol-like Languages, Progress in Theoretical Computer Science Series, Birkhauser, 1997.
• [21] A. M. Pitts. Nominal logic: a first order theory of names and binding. Information and Computation 183:165-193, 2003.
• [22] G. D. Plotkin and A. J. Power. Algebraic Operations and Generic Effects. In Proc. MFCSIT 2000, Applied Categorical Structures 11:69-94, 2003.
• [23] A. J. Power. Why Tricategories? Information and Computation 120:251-262, 1995.
• [24] A. J. Power. Enriched Lawvere theories. Theory and Applications of Categories 6:83-93, 1999.
• [25] A. J. Power. A Unified Category-Theoretic Approach to Variable Binding. In Proc. MERLIN 2003, ACM Digital Library, 2003.
• [26] A. J. Power. Countable Lawvere theories and Computational Effects. In Proc. MFCSIT 2004, Electronic Notes in Theoretical Computer Science 161:59-71, 2006.
• [27] D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series. Kluwer, 2002.
• [28] M. Tanaka. Abstract syntax and variable binding for linear binders. In Proc. MFCS 2000, LNCS 1893, pages 670-679, 2000.
• [29] M. Tanaka. Pseudo-Distributive Laws and a Unified Framework for Variable Binding. Edinburgh Ph.D. thesis, 2004.
• [30] M. Tanaka and J. Power. Pseudo-Distributive Laws and Axiomatics for Variable Binding. Higher-Order and Symbolic Computation 19:305-337, 2006.
• [31] M. Tanaka and J. Power. A Unified Category-Theoretic Formulation of Typed Binding Signatures. In Proc. MERLIN 2005, ACM Digital Library, 2005.
• [32] M. Tanaka and J. Power. A Unified Category-Theoretic Semantics for Binding Signatures in Substructural Logics. Journal of Logic and Computation, 16:5-25 , 2006.