Non-Uniform Hypercoherences
Pierre Boudes · Electronic Notes in Theoretical Computer Science · 2003
In [BE01], 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 [BE01]. We discuss the issue of sequentiality in this new model.