Abstract
We show that the category FinVect k of finite dimensional vector spaces and linear maps over any field k is (collectively) complete for the traced symmetric monoidal category freely generated from a signature, provided that the field has characteristic 0; this means that for any two different arrows in the free traced category there always exists a strong traced functor into FinVect k which distinguishes them. Therefore two arrows in the free traced category are the same if and only if they agree for all interpretations in FinVect k .
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
Bloom, S., Ésik, Z.: Iteration Theories, EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993)
Hasegawa, M.: Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 196–213. Springer, Heidelberg (1997)
Hasegawa, M.: Models of Sharing Graphs: A Categorical Semantics of let and letrec. Distinguished Dissertation Series. Springer, Heidelberg (1999), also available as Ph.D. thesis ECS-LFCS-97-360, University of Edinburgh (1997)
Hyland, M., Power, A.J.: Symmetric monoidal sketches and categories of wirings. Electr. Notes Theor. Comput. Sci, vol. 100, pp. 31–46 (2004)
Joyal, A., Street, R.: Braided tensor categories. Adv. Math. 102, 20–78 (1993)
Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Math. Proc. Cambridge Phil. Soc. 119(3), 447–468 (1996)
Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1971)
Pardo, D., Rabinovich, A.M., Trakhtenbrot, B.A.: Synchronous circuits over continuous time: feedback, reliability and completeness. Fundam. Inform. 62(1), 123–137 (2004)
Rabinovich, A.M., Trakhtenbrot, B.A.: Nets and data flow interpreters. In: Proc. Fourth Symp. on Logic in Computer Science, pp. 164–174. IEEE Computer Society Press, Washington (1989)
Simpson, A.K.: Categorical completeness results for the simply-typed lambda-calculus. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 414–427. Springer, Heidelberg (1995)
Simpson, A.K., Plotkin, G.: Complete axioms for categorical fixed-point operators. In: Proc. Fifteenth Symp. on Logic in Computer Science, pp. 30–41. IEEE Computer Society Press, Washington (2000)
Soloviev, S.V.: Proof of a conjecture of S. Mac Lane. Ann. Pure Appl. Logic 90, 101–162 (1997)
Statman, R.: Completeness, invariance, and definability. J. Symbolic Logic 47, 17–26 (1982)
Ştefǎnescu, G.: Network Algebra. Series in Discrete Mathematics and Theoretical Computer Science. Springer, Heidelberg (2000)
Trakhtenbrot, B.A.: On operators, realizable in logical nets. Doklady AN SSSR (Proceedings of the USSR Academy of Sciences) 112(6), 1005–1007 (1957)
Trakhtenbrot, B.A.: On the power of compositional proofs for nets: relationships between completeness and modularity. Fundam. Inform. 30(1), 83–95 (1997)
Yetter, D.N.: Functorial Knot Theory. World Scientific, Singapore (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hasegawa, M., Hofmann, M., Plotkin, G. (2008). Finite Dimensional Vector Spaces Are Complete for Traced Symmetric Monoidal Categories. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds) Pillars of Computer Science. Lecture Notes in Computer Science, vol 4800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78127-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-78127-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78126-4
Online ISBN: 978-3-540-78127-1
eBook Packages: Computer ScienceComputer Science (R0)