[TYPES] [Fwd: Preprint on Polarized Categories and Game Semantics]
Stephanie Weirich
sweirich at cis.upenn.edu
Tue Oct 26 11:05:07 EDT 2004
-------- Original Message --------
Subject: Preprint on Polarized Categories and Game Semantics
Date: Mon, 25 Oct 2004 01:58:59 -0400 (EDT)
From: Robert Seely <rags at math.mcgill.ca>
To: Categories List <categories at mta.ca>, Types List <types at cis.upenn.edu>
We'd like to announce the availability of the following preprint
at the website <www.math.mcgill.ca/rags/>
Polarized category theory, modules, and game semantics
by J.R.B. Cockett and R.A.G. Seely
ABSTRACT
Motivated by an analysis of Abramsky-Jagadeesan games, the paper
considers a categorical semantics for a polarized notion of two-player
games, a semantics which has close connections with the logic of (finite
cartesian) sums and products, as well as with the multiplicative
structure of linear logic. In each case, the structure is polarized, in
the sense that it will be modelled by two categories, one for each of
two polarities, with a module structure connecting them. These are
studied in considerable detail, and a comparison is made with a
different notion of polarization due to Olivier Laurent: there is an
adjoint connection between the two notions.
------------
We would point out (for readers interested in Type Theory) that this paper
gives a variant presentation of polarized linear logic (a presentation that
emphasizes slightly different aspects than Laurent's presentation, and results
in a subtly different version of polarized linear logic), and provides a
general semantics of that logic. The emphasis comes from the origins in
Abramsky-Jagadeesan games, rather than the Hyland-Ong games that underly
the intuitions in Laurent's approach. The result is a comprehensive analysis
of the structure of the polarized logic, including making explicit aspects
which are implicit in Laurent's approach (such as, for example, focalization).
One of the novel constructions our approach permits is what we call
"de-polarization": the construction of an unpolarized model from a
polarized one. We also describe three families of additive connectives,
which have somewhat different properties (and different polarities).
--
<rags at math.mcgill.ca>
<www.math.mcgill.ca/rags>
More information about the Types-list
mailing list