Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-30T23:31:47.376Z Has data issue: false hasContentIssue false
  • English
  • Français

The shuffle Hopf algebra and noncommutative full completeness

Published online by Cambridge University Press:  12 March 2014

R. F. Blute  and
P. J. Scott
R. F. Blute
Affiliation:
Department of Mathematics and Statistics, University of Ottawa, Ottawa, Ontario Kin 6N5, Canada. E-mail: [email protected]
P. J. Scott
Affiliation:
Department of Mathematics and Statistics, University of Ottawa, Ottawa, Ontario Kin 6N5, Canada. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a full completeness theorem for the multiplicative fragment of a variant of noncommutative linear logic, Yetter's cyclic linear logic (CyLL). The semantics is obtained by interpreting proofs as dinatural transformations on a category of topological vector spaces, these transformations being equivariant under certain actions of a noncocommutative Hopf algebra called the shuffle algebra Multiplicative sequents are assigned a vector space of such dinaturals, and we show that this space has as a basis the denotations of cut-free proofs in CyLL + MIX. This can be viewed as a fully faithful representation of a free *-autonomous category, canonically enriched over vector spaces.

This paper is a natural extension of the authors' previous work, “Linear Läuchli Semantics”, where a similar theorem is obtained for the commutative logic MLL + MIX. In that paper, we interpret proofs as dinaturals which are invariant under certain actions of the additive group of integers. Here we also present a simplification of that work by showing that the invariance criterion is actually a consequence of dinaturality. The passage from groups to Hopf algebras in this paper corresponds to the passage from commutative to noncommutative logic. However, in our noncommutative setting, one must still keep the invariance condition on dinaturals.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 63 , Issue 4 , December 1998 , pp. 1413 - 1436
Copyright
Copyright © Association for Symbolic Logic 1998

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Abé, K., Hopf algebras, Cambridge University Press, 1977.Google Scholar
[2] Abramsky, S., Semantics of interaction: an introduction to game semantics, in A. Pitts and P. Dybjer [40], pp. 1–31.Google Scholar
[3] Abramsky, S. and Jagadeesan, R., Games and full completeness for multiplicative linear logic, this Journal, vol. 59 (1994), no. 2, pp. 543–574.Google Scholar
[4] Abrusci, V. M., Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, this Journal, vol. 56 (1991), pp. 1403–1456.Google Scholar
[5] Bainbridge, E., Freyd, P., Scedrov, A., and Scott, P., Functorial polymorphism, Theoretical Computer Science, vol. 70 (1990), pp. 1403–1456.Google Scholar
[6] Barr, M., Duality of Banach spaces, Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 17 (1976), pp. 15–32.Google Scholar
[7] Barr, M., Duality of vector spaces, Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 17 (1976), pp. 3–14.Google Scholar
[8] Barr, M., *-autonomous categories, Lecture Notes in Mathematics, no. 752, Springer-Verlag, 1980.Google Scholar
[9] Barr, M., Noncommutative *-autonomous categories, preprint, 1993.Google Scholar
[10] Barr, M., Separability of tensor in Chu categories of vector spaces, Mathematical Structures in Computer Science, vol. 6 (1996), pp. 213–217.Google Scholar
[11] Benson, D. B., Bialgebras: some foundations for distributed and concurrent computation, Fundamenta Informaticae, vol. 12 (1989), pp. 427–486.Google Scholar
[12] Blute, R., Linearlogic, coherence anddinaturality, Theoretical Computer Science, vol. 115 (1993), pp. 3–41.Google Scholar
[13] Blute, R., Hopf algebras and linear logic, Mathematical Structures in Computer Science, vol. 6 (1996), pp. 189–212.Google Scholar
[14] Blute, R. F. and Scott, P. J., Linear Läuchli semantics, Annals of Pure and Applied Logic, vol. 77 (1996), pp. 101–142.Google Scholar
[15] Blute, R. F. and Scott, P. J., A noncommutative full completeness theorem (extended abstract), Electronic Notes in Theoretical Computer Science, vol. 3 (1996), Elsevier Science B. V. Google Scholar
[16] Cockett, J. R. B. and Seely, R. A. G., Proof theory for full intuitionistic linear logic, bilinear logic and mix categories, Theory and Applications of Categories, vol. 3 (1997), pp. 85–131.Google Scholar
[17] Coquand, T., Gunter, C., and Winskel, G., Domain-theoretic models of polymorphism, Information and Computation, vol. 81 (1989), no. 2, pp. 123–167.Google Scholar
[18] Danos, V., La logique linéaire appliquée à l'étude de divers processus de normalisation et principalement du λ-calcul, Thèse du doctorat, Université de Paris, 1990.Google Scholar
[19] Danos, V. and Régnier, L., The structure of multiplicatives, Archive for Mathematical Logic, vol. 28 (1989), pp. 181–203.Google Scholar
[20] Fleury, A., La règle d'échange: logique linéaire multiplicative tressée, Thèse du doctorat, U. Paris VII, 1996.Google Scholar
[21] Fleury, A. and Rétoré, C., The mix rule, Mathematical Structures in Computer Science, vol. 4 (1994), pp. 273–285.Google Scholar
[22] Girard, J. Y., The system F of variable types, fifteen years later, Theoretical Computer Science, vol. 45 (1986), no. 2, pp. 159–192.Google Scholar
[23] Girard, J. Y., Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.Google Scholar
[24] Girard, J. Y., Coherent Banach spaces, preprint and lectures delivered at Keio University, Linear Logic '96, 04 1996, 1996.Google Scholar
[25] Girard, J. Y., Lafont, Y., and Taylor, P., Proofs and types, Cambridge Tracts in Theoretical Computer Science, no. 7, 1989.Google Scholar
[26] Girard, J. Y., Scedrov, A., and Scott, P., Normal forms and cut-free proofs as natural transformations, Logic from computer science, Mathematical Science Research Institute Publications, no. 21, 1991, also available from http://hypatia.dcs.qmw.ac.uk, under Scott, pp. 217–241.Google Scholar
[27] Harnik, V. and Makkai, M., Lambek's categorical proof theory and Làuchli's abstract realizability, this Journal, vol. 57 (1992), pp. 200–230.Google Scholar
[28] Hazewinkel, M., Introductory recommendations for the study of Hopf algebras in mathematics and physics, CWI Quarterly, vol. 4 (1991), no. 1, Centre for Mathematics and Computer Science, Amsterdam.Google Scholar
[29] Hyland, J. M. E., Game semantics, in A. Pitts and P. Dybjer [40], pp. 131–184.Google Scholar
[30] Hyland, J. M. E. and Ong, C.-H. L., On full abstraction for PCF, to appear, 1995.Google Scholar
[31] Joni, S. and Rota, G. C., Coalgebras and bialgebras in combinatorics, Studies in Applied Mathematics, vol. 61 (1979), pp. 93–139.Google Scholar
[32] Joyal, A., Une théorie combinatoire des sériesformelles, Advances in Mathematics, vol. 42 (1981), pp. 1–82.Google Scholar
[33] Lambek, J., Bilinear logic in algebra and linguistics, Advances in linear logic, London Mathematical Society Series, no. 222, Cambridge University Press, Cambridge, 1995.Google Scholar
[34] Läuchli, H., An abstract notion of realizability for which intuitionistic predicate calculus is complete, lntuitionism and proof theory, North-Holland, 1970, pp. 227–234.Google Scholar
[35] Lawvere, F. W., Equality in hyperdoctrines and comprehension schema as an adjoint functor, Proceedings of the New York symposium on applications of categorical algebra (Heller, A., editor), American Mathematical Society, pp. 1–14.Google Scholar
[36] Lawvere, F. W., Adjointness in foundations, Dialectica, vol. 23 (1969), pp. 281–296.Google Scholar
[37] Lefschetz, S., Algebraic topology, American Mathematical Society Colloquium Publications, no. 27, 1963.Google Scholar
[38] Majid, S., Physics for algebraists: noncommutative and noncocommutative Hopf algebras by a bicrossproduct construction, Journal of Algebra, vol. 130 (1990), pp. 17–64.Google Scholar
[39] Majid, S., Quasitriangular Hopf algebras and Yang-Baxter equations, International Journal of Modern Physics, vol. 5 (1990), pp. 1–91.Google Scholar
[40] Pitts, A. and Dybjer, P. (editors), Semantics and logics of computation, Publications of the Newton Institute, Cambridge University Press, 1997.Google Scholar
[41] Plotkin, G., Lambda definability in the full type hierarchy, To H. B. Curry, essays on combinatory logic, Lambda calculus, and formalism, Academic Press, 1980, pp. 363–373.Google Scholar
[42] Plotkin, G., 08 1996, private communication.Google Scholar
[43] Plotkin, G. and Abadi, M., A logic for parametric polymorphism, Typed Lambda calculus and applications, Lecture Notes in Computer Science, no. 664, Springer-Verlag, 1993, pp. 361–375.Google Scholar
[44] Retoré, C., Calcul de Lambek et logique linéaire, Traitement Automatique des Langues, vol. 37, no. 2, pp. 39–70.Google Scholar
[45] Retoré, C., Des réseaux de demonstration pour la linguistique, manuscript, 1996.Google Scholar
[46] Rosenthal, K. I., *-autonomous categories of bimodules, Journal of Pure and Applied Algebra, vol. 97 (1994), pp. 189–202.Google Scholar
[47] Schmitt, W., Antipodes and incidence coalgebras, Journal of Combinatorial Theory, vol. 46 (1987), pp. 264–290.Google Scholar
[48] Schmitt, W., Hopf algebras of combinatorial structures, Canadian Journal of Mathematics, vol. 45 (1993), pp. 412–428.Google Scholar
[49] Sweedler, M., Hopf algebras, Benjamin Press, 1969.Google Scholar
[50] Treves, F., Topological vector spaces, distributions and kernels, Academic Press, 1967.Google Scholar
[51] Ulbrich, K., On Hopf algebras and rigid monoidal categories, Israel Journal of Mathematics, vol. 71 (1989), pp. 252–256.Google Scholar
[52] Yetter, D., Quantales and (noncommutative) linear logic, this Journal, vol. 55 (1990), pp. 41–64.Google Scholar