Fock Space

To: linear@cs.stanford.edu
Subject: Fock Space
From: blute@triples.math.mcgill.ca (Richard Blute)
Date: Thu, 14 Jul 94 14:49:05 EDT
Approved: types@dcs.gla.ac.uk


The following paper is available by anonymous ftp from triples.math.mcgill.ca,
in the directory pub/blute. Anyone without ftp access can of course write to
me at the above address.

Cheers,
Rick Blute

              Fock Space: A Model of Linear Exponential Types

                   R. Blute     P. Panangaden    R. Seely

                                ABSTRACT

It has been observed by several people that, in certain contexts, the free 
symmetric algebra construction can provide a model of the linear modality !.
This construction arose independently in quantum physics, where it is
considered as a canonical construction in quantum field theory. 
In this context, it is known as (bosonic) Fock space. Fock space
is used to analyze such quantum phenomena as the annihilation and creation of 
particles. There is a strong intuitive connection to the principle of 
renewable resource, which is the philosophical interpretation of the linear 
modalities.

In this paper, we examine Fock space in several categories of vector spaces.
We first consider vector spaces, where the Fock construction 
induces a model of the $\tensor, \with, !$ fragment in the category 
of symmetric algebras. When considering Banach spaces, the Fock construction 
provides a model of a weakening cotriple in the sense of Jacobs.
While the models so obtained have weaker properties, it is closer
in practice to the structures considered by physicists. In this case, Fock 
space has a natural interpretation as a space of holomorphic functions. This
suggests that the ``nonlinear'' functions we arrive at via Fock
space are not merely continuous but analytic.

Finally, we also consider fermionic Fock space, which corresponds algebraically
to skew symmetric algebras. By considering fermionic Fock space
on the category of finite-dimensional vector spaces, we obtain a model of
full propositional linear logic, although the model is somewhat degenerate
in that certain connectives are equated.

This paper is a revised and expanded version of an earlier draft entitled
``Holomorphic Models of Exponential Types in Linear Logic'', appearing in the
MFPS IX proceedings, Springer LNCS. In particular, it corrects 
an error therein. It is stated there that Fock space is functorial 
on the category of Banach spaces and bounded linear maps. Instead 
one must consider the category of contractive maps, as discussed in section 5.