page 1  (15 pages)
2to next section

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 Q-respecting 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 quantale-valued sets," thus constructing a class of models of classical linear logic that approximate what locale-valued sets are to intuitionistic logic. There have been previous attempts at constructing categories of quantale-valued 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 well-known 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 5-uple (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.