my groupoid model

[Paul Taylor <pt@dcs.qmw.ac.uk>]

Francois Lamarche says:
> I still think that if I started working again in this field,
> the problem I would zero in would be to get rid of the permutation groups,


This would be a great pity.  


Girard's coherence spaces (see "Proofs and Types"), ordinary relational
algebra (in which Shroeder identified the par, writing   +,   for it,
I think,  in 1895)  and my model with groupoids all illustrate a common
theme in the workings of models of linear logic.

In all of these structures, there are extremely natural ways of defining
the structure on disjoint unions and cartesian products,  and of turning
the structure inside out or upside down.  These turn out to be the additive,
multiplicative and negative connectives in linear logic.

There are less natural ways of defining the structure on powersets,
finite powersets and other variations on this theme.  These are the
exponentials.  It is important to note that there are several different
exponential operations available to interpret ! and ? .

Girard got function spaces out of such constructions (as did Francois,
myself and numerous other people).   What I hope to show soon is how to
get higher order logic too.

Paul