Musings Around the Geometry of Interaction and Coherence
Jean Goubault-Larrecq
ABSTRACT
This talk will explore the geometry of interaction from the angle
that it provides a calculus of (finite) paths through typed
lambda-terms, or rather through infinite objects such as Boehm trees.
The key to reconstructing trees from sets of paths is a notion of
coherence between paths, as in coherence spaces, or in event
structures. In the case of multiplicative linear logic (with
fixpoint), the correspondence is perfect, and can be taken as a
foundation of a categorical semantics; in particular, we get a
compact-closed category with a reflexive object. This is obtained as
the Danos-Rtions that we shall
introduce, and study.) Under the latter assumption, DR(M) is then a
kind of symmetrized version of Abramsky and coauthors' GOI situation
construction over a category IG(M) (the so-called inductive groupoid
associated with M) that is well-known in the monoid community.
A bit surprisingly, we shall show that DR(M) cannot be turned into a
categorical model of the rest of linear logic. DR(M) has no terminal
object, no initial object, no product and no coproduct unless M is
trivial. So additives don't exist inside DR(M). Exponentials suffer a
similar fate. One may argue that proper exponentials should link
DR(M) with its category of internal (co)commutative comonoids of
DR(M). Unfortunately, the only internal (co)commutative comonoid in
DR(M) is the trivial one, so that DR(M) is a new-Lafont category in
the sense of Melliial. This does not
prevent DR(M) from being an interesting model. While not all
categorical equalities hold, enough do. In fact just enough hold so
as to yield a good platform for optimal lambda-reduction. I won't
stress this, as the topic of my talk is rather the quest for
categorical (hence very extensional) models of classical linear logic
with fixpoints---which should have an interpretation in terms of
paths.
While coherence was central to the construction of DR(M), coherence
again is the key to building a model of full classical logic with
fixpoints, by considering a slight variant of Hu and Joyal's
coherence completion Coh(DR(M)) of DR(M). The latter mixes the nice
structure of coherence spaces with the preexisting structure of
DR(M). I'll argue that Coh(DR(M)) can be seen as a way of describing
all paths through proof terms by arranging them into several tracing
paper layers, with conditions of coherence inside each layer (from
DR(M)) and between each layer (from the Coh construction) so that
they overlay nicely.