Hostname: page-component-74656f9884-c52kr Total loading time: 0 Render date: 2026-11-08T23:16:13.871Z Has data issue: false hasContentIssue false
  • English
  • Français

On traced monoidal closed categories

Published online by Cambridge University Press:  01 April 2009

MASAHITO HASEGAWA
MASAHITO HASEGAWA*
Affiliation:
Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502, Japan Email: hassei@kurims.kyoto-u.ac.jp
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

The structure theorem of Joyal, Street and Verity says that every traced monoidal category arises as a monoidal full subcategory of the tortile monoidal category Int. In this paper we focus on a simple observation that a traced monoidal category is closed if and only if the canonical inclusion from into Int has a right adjoint. Thus, every traced monoidal closed category arises as a monoidal co-reflexive full subcategory of a tortile monoidal category. From this, we derive a series of facts for traced models of linear logic, and some for models of fixed-point computation. To make the paper more self-contained, we also include various background results for traced monoidal categories.

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 2 , April 2009 , pp. 217 - 244
Copyright
Copyright © Cambridge University Press 2008

References

Abramsky, S. (1996) Retracing some paths in process algebra. In: Proc. Concurrency Theory. Springer-Verlag Lecture Notes in Computer Science 1119 1–17.CrossRefGoogle Scholar
Abramsky, S., Haghverdi, E. and Scott, P. J. (2002) Geometry of Interaction and linear combinatory algebras. Mathematical Structures in Computer Science 12 (5)625–665.CrossRefGoogle Scholar
Abramsky, S. and Jagadeesan, R. (1994) New foundations for the Geometry of Interaction. Inf. Comput. 111 (1)53–119.CrossRefGoogle Scholar
Barber, A. and Plotkin, G. (1997) Dual intuitionistic linear logic (manuscript). An earlier version available as Technical Report ECS-LFCS-96-347, LFCS, University of Edinburgh.Google Scholar
Barr, M. (1991) *-autonomous categories and linear logic. Mathematical Structures in Computer Science 1 159–178.CrossRefGoogle Scholar
Benton, N. (1995) A mixed linear non-linear logic: proofs, terms and models. In: Proc. Computer Science Logic. Springer-Verlag Lecture Notes in Computer Science 933 121–135.CrossRefGoogle Scholar
Bierman, G. M. (1995) What is a categorical model of intuitionistic linear logic? In: Proc. Typed Lambda Calculi and Applications. Springer-Verlag Lecture Notes in Computer Science 902 78–93.CrossRefGoogle Scholar
Bloom, S. and Ésik, Z. (1993) Iteration Theories, EATCS Monographs on Theoretical Computer Science, Springer-Verlag.CrossRefGoogle Scholar
Blute, R. F., Cockett, J. R. B. and Seely, R. A. G. (2000) Feedback for linearly distributive categories: traces and fixpoints. J. Pure Appl. Algebra 154 27–69.CrossRefGoogle Scholar
Chirica, L. M. and Martin, D. F. (1979) An order-algebraic definition of Knuthian semantics. Mathematical Systems Theory 13 1–27.CrossRefGoogle Scholar
Coccia, M., Gadducci, F. and Montanari, U. (2002) GS-Λ theories: a syntax for higher-order graphs. In: Proc. Category Theory and Computer Science. Electronic Notes in Theoretical Computer Science 69.Google Scholar
Cockett, J. R. B. and Seely, R. A. G. (1999) Linearly distributive functors. J. Pure Appl. Algebra 143 155–203.CrossRefGoogle Scholar
Freedman, M. H., Kitaev, A. and Wang, Z. (2002) Simulation of topological field theories by quantum computers. Commun. Math. Phys. 227 587–603.CrossRefGoogle Scholar
Girard, J.-Y. (1987) Linear logic. Theoretical Computer Science 50 1–102.CrossRefGoogle Scholar
Girard, J.-Y. (1989) Geometry of Interaction I: interpretation of system F. In: Proc. Logic Colloquium '88 221–260.CrossRefGoogle Scholar
Haghverdi, E. (2000) A Categorical Approach to Linear Logic, Geometry of Interaction and Full Completeness, Ph.D. thesis, University of Ottawa.Google Scholar
Haghverdi, E. and Scott, P. J. (2006) A categorical model for the geometry of interaction. Theoretical Computer Science 350 (2–3) 252–274.CrossRefGoogle Scholar
Hasegawa, M. (1997) Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi. In: Proc. Typed Lambda Calculi and Applications. Springer-Verlag Lecture Notes in Computer Science 1210 196–213.CrossRefGoogle Scholar
Hasegawa, M. (1999) Models of Sharing Graphs: A Categorical Semantics of let and letrec, Distinguished Dissertations Series, Springer-Verlag.Google Scholar
Hasegawa, M. (2000) A short proof of the uniqueness of trace on tortile categories (manuscript, available from the author's web page).Google Scholar
Hasegawa, M. (2004) The uniformity principle on traced monoidal categories. Publ. Res. Inst. Math. Sci. 40 (3)991–1014.CrossRefGoogle Scholar
Houston, R. (2008) Finite products are biproducts in a compact closed category. J. Pure Appl. Algebra 212 394–400.CrossRefGoogle Scholar
Hyland, M. and Schalk, A. (2003) Glueing and orthogonality for models of linear logic. Theoretical Computer Science 294 (1–2) 183–231.CrossRefGoogle Scholar
Joyal, A. and Street, R. (1991) The geometry of tensor calculus, I. Adv. Math. 88 55–113.CrossRefGoogle Scholar
Joyal, A. and Street, R. (1993) Braided tensor categories. Adv. Math. 102 20–78.CrossRefGoogle Scholar
Joyal, A., Street, R. and Verity, D. (1996) Traced monoidal categories. Math. Proc. Cambridge Phils. Soc. 119 447–468.CrossRefGoogle Scholar
Katsumata, S. (2008) Attribute grammars and categorical semantics. In: Proc. International Colloquium on Automata, Languages and Programming. Springer-Verlag Lecture Notes in Computer Science. 5126 271–282.CrossRefGoogle Scholar
Katsumata, S. and Nishimura, S. (2006) Algebraic fusion of functions with an accumulating parameter and its improvement. In: Proc. International Conference on Functional Programming 227–238.CrossRefGoogle Scholar
Kelly, G. M. (1974) Doctrinal adjunction. In: Proc. Sydney Category Theory Seminar. Springer-Verlag Lecture Notes in Computer Science 420 257–280.Google Scholar
Kelly, G. M. and Laplaza, M. L. (1980) Coherence for compact closed categories. J. Pure Appl. Algebra 19 193–213.CrossRefGoogle Scholar
Knuth, D. E. (1968) Semantics of context-free languages. Mathematical Systems Theory 2 (2)127–145.CrossRefGoogle Scholar
Lambek, J. and Scott, P. J. (1986) Introduction to Higher Order Categorical Logic, Cambridge University Press.Google Scholar
Mac Lane, S. (1971) Categories for the Working Mathematician, Graduate Texts in Mathematics 5, Springer-Verlag.CrossRefGoogle Scholar
Melliès, P.-A. (2003) Categorical models of linear logic revisited. To appear in Theoretical Computer Science.Google Scholar
Melliès, P.-A. (2004) Asynchronous games 3: an innocent model of linear logic. In: Proc. Category Theory and Computer Science. Electronic Notes in Theoretical Computer Science 122 171–192.CrossRefGoogle Scholar
Melliès, P.-A. (2006) Functorial boxes in string diagrams. In: Proc. Computer Science Logic. Springer-Verlag Lecture Notes in Computer Science 4207 1–30.CrossRefGoogle Scholar
Melliès, P.-A. and Tabareau, N. (2007) Resource modalities in game semantics. In: Proc. 22nd Logic in Computer Science 389–398.CrossRefGoogle Scholar
Milner, R. (1994) Action calculi V: reflexive molecular forms (with appendix by O. Jensen). Manuscript, LFCS, University of Edinburgh.Google Scholar
Penrose, R. and Rindler, R. (1984) Spinors and Space-Time, Vol. 1, Cambridge University Press.CrossRefGoogle Scholar
Seely, R. A. G. (1989) Linear logic, *-autonomous categories and cofree coalgebras. In: Categories in Computer Science. AMS Contemp. Math. 92 371–389.CrossRefGoogle Scholar
Selinger, P. (2007) Dagger compact closed categories and completely positive maps (extended abstract). In: Proc. International Workshop on Quantum Programming Languages. Electronic Notes in Theoretical Computer Science 170 139–163.CrossRefGoogle Scholar
Shum, M.-C. (1994) Tortile tensor categories. J. Pure Appl. Algebra 93 57–110.CrossRefGoogle Scholar
Simpson, A. (1993) A characterisation of the least-fixed-point operator by dinaturality. Theoretical Computer Science 118 (2)301–314.CrossRefGoogle Scholar
Simpson, A. and Plotkin, G. (2000) Complete axioms for categorical fixed-point operators. In: Proc. 15th Logic in Computer Science 30–41.CrossRefGoogle Scholar
Ştefanescu, G. (2000) Network Algebra, Discrete Mathematics and Theoretical Computer Science Series, Springer-Verlag.CrossRefGoogle Scholar
Yetter, D. N. (2001) Functorial Knot Theory, World Scientific.CrossRefGoogle Scholar