[Prev][Next][Index][Thread]

Banach Spaces & Linear Logic

[This digest includes three related messages.
-- Phil Wadler, moderator, Types Forum]

---------------------------------------------------------------------------
 From: Gerry Allwein <gtall@edu.indiana.cica.ogre>
 Date: Wed, 28 Jul 1993 06:59:14 -0500

Folks, does anyone know of a paper(s) relating linear logic and banach spaces?

Gerry

---------------------------------------------------------------------------
 Date: Fri, 30 Jul 93 13:00:42 EDT
 From: Richard Blute <RBLUTE@acadvm1.uottawa.ca>

Gerry Allwein asks for a reference on the relation between linear logic
and Banach spaces. At this year's MFPS conference, Prakash Panangaden, Robert
Seely and I presented a paper entitled "Holomorphic Models of Exponential
Types in Linear Logic". In this paper, we build a model of the tensor-!
fragment in the category of commutative Banach algebras. Hopefully, we will be
announcing the completed paper soon.

One of the main distinctions between Banach spaces (and Hilbert spaces)
is that the existence of a norm allows one to discuss convergent sequences,
power series (hence holomorphic functions), etc. The specific construction
we use to model ! is called Fock space. Fock space was introduced in quantum
field theory as a framework for modelling the annihilation and creation of
particles. There is a pleasing analogy here between such ideas and that
of infinitely renewable resource.

Finally, the Fock space associated to a Banach space or Hilbert space
has a concrete representaton as a space of holomorphic functions,
suitably defined.Thus, the Kleisli category can reasonably be thought of
as a category of generalized holomorphic functions.

Rick Blute

---------------------------------------------------------------------------
 Date: Fri, 30 Jul 93 18:16:33 EDT
 From: Richard Blute <RBLUTE@acadvm1.uottawa.ca>

Half of a sentence of my last note somehow vanished so please let
me clarify one issue.

The point of the second paragraph is that Banach spaces and Hilbert spaces
have a notion of norm, whereas ordinary vector spaces do not. Thus, the
notions of convergent sequence, power series, etc. make sense in either
a Banach Space or Hilbert space.

Rick Blute