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

Fwd: Thomas Streicher's message




In reply to Thomas' message:

1. ``Making a category out of Geometry of Interaction'' was done by me
in October 1991. For the ``product form of GoI'' this appeared in my
paper with Radha Jagadeesan on ``New Foundations for the Geometry of
Interaction'' in LICS '92.
I also considered the ``coproduct form'', i.e. the Girard GoI
(henceforth GGI). The problems Thomas mentions with this are exactly
those which arise with correctness of GGI, which is why the correctness
of the intepretation is stated with restrictions in Girard's paper on
''Geometry of Interaction I''. I talked about this in my tutorial
lecture and talk at LICS 92.

2. The games and history-free strategy semantics of Linear Logic  given
by myself and Radha agree EXACTLY with  GGI at the level of
interpretation of proofs. That is, the partial functions on moves
determining the history-free strategies are exactly the functions
assigned to proofs in GGI (where GGI is cut down to the essential
content of partial 1-1 maps); moreover, the execution formula coincides
exactly with the composition of strategies.  All of this is laid out
very clearly and explicitly as far as the multiplicatives are concerned
in my paper with Radha on ``Games and Full Completeness for MLL''.

3. The history-free semantics for the exponentials is not discussed in
that paper. It was worked out subsequently by us, and will appear in a
paper currently under preparation. This history-free semantics again
coincides exactly with that of GGI at the level of interpretation of
proofs. (Incidentally, the interpretation of the exponentials could also
be said to be that of Blass - going all the way back to 1972!). The key
point is that the games provide the missing notion of type, which allows
us to make an honest model out of GGI, and more, to get Full
Completeness theorems, previously completely out of reach.

4. This leaves the question raised by Thomas: how do we overcome the
commutation problems with the exponentials? This was quite non-trivial -
it took us about 3 months to find the right definitions. Briefly, we
enrich the notion of game with a specified automorphism group, and
impose an equivalence on strategies using these groups - the equivalence
is ``logical relations extended in time''. This solves all commutation
problems, and opens up the possibility of very strong full completeness
results for various intuitionistic fragments; these to be described in
the forthcoming paper. Incidentally, products ARE well-defined in the
co-Kleisli category.

In slightly more detail. The refined version of a category of games G we
use has objects A with an extra component G_A, where
G_A is a subgroup of Aut(A), the automorphism group of A in the category
G^e of games as embeddings, as described in my previous paper with
Radha. Thus an automorphism is a permutation on the alphabet which
preserves all the structure of the game.
This group G_A induces an equivalence on positions in A : s equiv t if
e*(s) = t for some e in G_A, where e* is the extension of e to sequences.

Now given two strategies sigma, tau on A, we define a relation sigma
equiv tau iff:
for all sab in sigma, ta'b' in tau of even length :  if sa equiv ta'
then sab equiv ta'b'.
This is a PARTIAL Equivalence relation on strategies. Morphisms in the
category are then equivalence classes of strategies satisfying the
partial equiv. relation. Of course, one must check that the relation is
compatible with the various constructions in the category; the
interesting case to check is composition.
The fact that sigma equiv sigma expresses a ``representation
independence'' property of strategies; the fact that sigma equiv tau
expresses that they are the same modulo insignificant coding conventions.

To complete the picture, we must say how the various constructions act
on the permutation groups. The multiplicatives do so trivially, just
combining permutations by disjoint union. Negation does nothing at all
to the permutation group.
For the exponentials, we define the moves of !A as
omega times M_A. The index i in (i,a) delineates which copy of A we are
in. The history-free monad structure etc. for !A works on these indices
as described by Blass, or as in GGI (but we insist that !A is negative;
only opening moves by Opponent are allowed). To define G_!A, we take all
permutations alpha x beta, where alpha is an arbitrary permutation on
omega, and beta is in G_A.
It is quite a thing of beauty to see how all this works out, e.g. for
the contraction (comultiplication) morphisms
 !A -> !A (x) !A.
Once you have done some of the calculations, you should be convinced
that these definitions are exactly right.
To repeat, products work on the nose in the history-free co-Kleisli
category. This is why GGI works for the lambda calculus, despite the
correctness problems with full Linear Logic.

All the best,

Samson Abramsky