
Electronic Notes in Theoretical Computer Science 1 (1995) to appear
Generalizing Coherence Spaces and
Hypercoherences
<_author_search_(fran?cois lamarche)>Fran?cois Lamarche
Department of Computing
Imperial College
180 Queen's Gate
London SW7 UK
Abstract
Let Q be a Girard quantale. In other words Q is a complete lattice which also has the structure of a ?autonomous category. For every n 2 f3; 4; 5; : : : ; !g we define a category of sets with values in Q and Qrespecting relations" which gives us a model of full classical linear logic, thus generalizing both the category of coherence spaces [9] and that of hypercoherences [7].
In this paper we present categories of Girard quantalevalued sets," thus constructing a class of models of classical linear logic that approximate what localevalued sets are to intuitionistic logic. There have been previous attempts at constructing categories of quantalevalued sets [14,6], but ours differs primarily in that morphisms emulate relations between the quantalevalued sets we define, as opposed to functions. If one's goal is to construct ?autonomous categories this should come as no surprise since the canonical model of classical linear logic that has sets as objects has relations as morphisms. A very good sign that something about our model is right, is that we end up generalizing two wellknown models of classical linear logic, namely coherent domains [9] and hypercoherences [7]. Independently of the fact that we do get interesting new models, this is an illustration of the slogan good generalization brings better understanding".
1 ?Autonomous Posets and Girard Quantales.
We will use Occam's Razor and try to get a definition for the structures that interest us which is as simple to state (and thus verify) as possible. We start with a 5uple (Q; 1; ?; (?)?; C) where
(i) (Q; 1; ?) is a commutative monoid.
(ii) (?)? is an involution on the set Q, i.e. ?? = .
(iii) C ae Q is a subset with 1 2 C.
c 1995 Elsevier Science B. V.