Skip to main content
SpringerLink
Log in

Holomorphic models of exponential types in linear logic

  • Conference paper
  • First Online:
Mathematical Foundations of Programming Semantics (MFPS 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 802))

Abstract

In this paper we describe models of several fragments of linear logic with the exponential operator ! (called Of course) in categories of linear spaces. We model ! by the Fock space construction in Banach (or Hilbert) spaces, a notion originally introduced in the context of quantum field theory. Several variants of this construction are presented, and the representation of Fock space as a space of holomorphic functions is described. This also suggests that the “non-linear” functions we arrive at via! are not merely continuous, but analytic.

Research supported in part by FCAR of Quebec.

Research supported in part by an NSERC Research Grant.

Research supported in part by an NSERC Research Grant and by FCAR of Quebec.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrusci, V.M. “Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic”, Journal of Symbolic Logic 56 (1991) 1403–1451.

    Google Scholar 

  2. Ahlfors, L.V. Complex Analysis. McGraw-Hill, New York, 1966, second edition. (First edition 1953).

    Google Scholar 

  3. Ashtekar, A. and A. Magnon-Ashtekar “A geometrical approach to external potential problems in quantum field theory”, Journal of General Relativity and Gravitation 12 (1980) 205–223.

    Google Scholar 

  4. Baez, J.C., I.E. Segal and Z. Zhou Introduction to algebraic and constructive quantum field theory. Princeton University Press, Princeton, New Jersey, 1992.

    Google Scholar 

  5. Bargmann, V. “On a Hilbert space of analytic functions and an associated integral transform”, Communications in Pure and Applied Mathematics 14 (1961) 187–214.

    Google Scholar 

  6. Barr, M. “Duality of vector spaces”, Cahiers de Topologie et Géometrie Differentielle 17 (1976) 3–14.

    Google Scholar 

  7. Barr, M. “Duality of Banach spaces”, Cahiers de Topologie et Géometrie Differentielle 17 (1976) 15–52.

    Google Scholar 

  8. Barr, M. *Autonomous Categories. Lecture Notes in Mathematics 752, Springer-Verlag, Berlin, Heidelberg, New York, 1979.

    Google Scholar 

  9. Barr, M. “*autonomous categories and linear logic”, Mathematical Structures in Computer Science 1 (1991) 159–178.

    Google Scholar 

  10. Benton, B.N., G. Bierman, V. de Paiva, and M. Hyland “Term assignment for intuitionistic linear logic (preliminary report)”, Preprint, University of Cambridge, 1992.

    Google Scholar 

  11. Blute, R.F. “Proof nets and coherence theorems”, in Categories and Computer Science, Paris 1991, Lecture Notes in Computer Science 530, Springer-Verlag, Berlin, Heidelberg, New York, 1991.

    Google Scholar 

  12. Blute, R.F. “Linear Logic, Coherence and Dinaturality”, to appear in Theoretical Computer Science.

    Google Scholar 

  13. Blute, R. “Linear Topology, Hopf Algebras and *-autonomous Categories”, preprint, McGill University (1993)

    Google Scholar 

  14. Blute, R. “Braided Proof Nets and Categories”, in preparation, (1993).

    Google Scholar 

  15. Blute, R.F., J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble “Natural deduction and coherence for weakly distributive categories”, Preprint, McGill University, 1992. (Submitted to JPAA)

    Google Scholar 

  16. Blute, R.F., J.R.B. Cockett, and R.A.G. Seely “ ! and ? for weakly distributive categories: Storage as tensorial strength”, preprint, McGill University, in preparation.

    Google Scholar 

  17. Cigler, J., V. Losert, P. Michor Banach Modules and Functors on Categories of Banach Spaces. Dekker, 1979

    Google Scholar 

  18. Cockett, J.R.B. and R.A.G. Seely “Weakly distributive categories”, in M.P. Fourman, P.T. Johnstone, A.M. Pitts, eds., Applications of Categories to Computer Science, London Mathematical Society Lecture Note Series 177 (1992) 45–65.

    Google Scholar 

  19. Conway, J. A Course in Functional Analysis. Springer Verlag Graduate Texts in Mathematics 96, (1990)

    Google Scholar 

  20. Freyd, P.J. Abelian Categories: An introduction to the theory of functors. Harper and Row, New York, 1964.

    Google Scholar 

  21. Geroch, R. Mathematical Physics. University of Chicago Press, 1985.

    Google Scholar 

  22. Girard, J.-Y. “Linear logic”, Theoretical Computer Science 50 (1987) 1–102.

    Google Scholar 

  23. Girard, J.-Y. “Geometry of interaction I: Interpretation of system F”, Proceedings of ASL meeting, Padova, 1988.

    Google Scholar 

  24. Girard, J.-Y. and Y. Lafont “Linear logic and lazy computation”, in Tapsoft'87, 2, Lecture Notes in Computer Science 250, Springer-Verlag, Berlin, Heidelberg, New York, 1987, 52–66.

    Google Scholar 

  25. Girard, J.-Y., A. Scedrov, and P.J. Scott “Bounded linear logic”, Theoretical Computer Science 97 (1992) 1–66.

    Google Scholar 

  26. Gunning, R. Introduction to Holomorphic functions of several variables, Volume 1: Function theory. Mathematics Series, Wadsworth and Brooks/Cole, Belmont CA, 1990.

    Google Scholar 

  27. Itzykson, J, and J. Zuber Introduction to Quantum Field Theory. McGraw-Hill, New York, 1980.

    Google Scholar 

  28. Kadison, R.V. and J.R. Ringrose Fundamentals of the Theory of Operator Algebras. Academic Press, New York, 1983

    Google Scholar 

  29. Kelly, G.M. and M. La Plaza, “Coherence for Compact Closed Categories”, Journal of Pure and Applied Algebra 19 (1980) 193–213.

    Google Scholar 

  30. Lang, S. Algebra. Addison-Wesley Pub. Co., Reading, Menlo Park, London, Don Mills, 1965.

    Google Scholar 

  31. Lefschetz, S. Algebraic Topology. AMS Colloquium Publications 27, 1941.

    Google Scholar 

  32. Mac Lane, S. Categories for the Working Mathematician. Graduate Texts in Mathematics 5, Springer-Verlag, Berlin, Heidelberg, New York, 1971

    Google Scholar 

  33. Martí-Oliet, N. and J. Meseguer “From Petri nets to linear logic”, in D.H. Pitt et al., eds. Category Theory and Computer Science, Manchester 1989, Lecture Notes in Computer Science 389, Springer-Verlag, Berlin, Heidelberg, New York, 1989.

    Google Scholar 

  34. de Paiva, V.C.V. “A Dialectica-like model of linear logic”, in D.H. Pitt et al., eds., Category Theory and Computer Science, Lecture Notes in Computer Science 389, Springer-Verlag, Berlin, Heidelberg, New York, 1989.

    Google Scholar 

  35. Panangaden, P. “Positive and negative frequency decompositions in curved spacetimes”, Journal of Mathematical Physics 20 (1979) 2506–2514.

    Google Scholar 

  36. Panangaden, P. “Propagators and Renormalization of Quantum Field Theory in Curved Spacetimes.”, Ph.D. Thesis, Physics Department, University of Wisconsin-Milwaukee, 1980. Available through University Microfilms International, Ann Arbor.

    Google Scholar 

  37. Seely, R.A.G. “Linear logic, *-autonomous categories and cofree coalgebras”, in J. Gray and A. Scedrov (eds.), Categories in Computer Science and Logic, Contemporary Mathematics 92 (Am. Math. Soc. 1989).

    Google Scholar 

  38. Segal, E. “Mathematical characterization of the physical vacuum for linear Bose-Einstein fields”, Illinois Journal of Mathematics 6 (1962) 500–523.

    Google Scholar 

  39. Takesaki M. Theory of Operator Algebras. Springer-Verlag, Berlin, Heidelberg, New York, 1979.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of Ottawa, K1N 6N5, Ottawa, Canada

    R. F. Blute

  2. School of Computer Science, McGill University, H3A 2A7, Montreal, Canada

    Prakash Panangaden

  3. Department of Mathematics, McGill University, H3A 2K6, Montreal, Canada

    R. A. G. Seely

Authors
  1. R. F. Blute
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Prakash Panangaden
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. R. A. G. Seely
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stephen Brookes Michael Main Austin Melton Michael Mislove David Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Blute, R.F., Panangaden, P., Seely, R.A.G. (1994). Holomorphic models of exponential types in linear logic. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1993. Lecture Notes in Computer Science, vol 802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58027-1_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-58027-1_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58027-0

  • Online ISBN: 978-3-540-48419-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation