Non uniform hypercoherences
Conférence CTCS 2002
In [BE99], Bucciarelli and Ehrhard propose a general tool for
building a wide class of models of linear logic where a formula is
interpreted as a set (the web) together with a kind of phase valued
"coherence relation’’. These interpretations are non uniform in the
sense that the semantics of a proof makes no assumption about the
behaviour of its possible counter-proofs, unlike e.g. in the usual
stable semantics where the argument of a stable functional is always a
stable function. However, until now, it was suspected that this
non-uniformity necessarily induces a kind of non-determinism, namely
that a "clique’’ and an "anti-clique’’ could have more than one
point in common. We provide a new non-uniform semantics of linear
logic where this property of determinism is preserved. This is done by
constructing the co-free exponential in the "non-uniform coherence
space’’ framework described at the end of [BE99]. We discuss
the issue of sequentiality in this new model.
Documents joints
- version préliminaire (PDF – 307.2 ko)
- ps.gz (GZ – 215 ko)