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.
Fock Space: A Model of Linear Exponential Types
R. Blute P. Panangaden R. Seely
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
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.