Non uniform (hyper/multi)coherence spaces

TL;DR

This paper introduces non-uniform hypercoherence and multicoherence spaces, reconstructing missing vertices in coherence semantics to better compare with other models like game semantics, using a co-free exponential construction.

Contribution

It develops a new non-uniform coherence space semantics with a co-free exponential, allowing reconstruction of missing vertices and deterministic interactions, extending previous uniform models.

Findings

Reconstruction of missing vertices in coherence semantics.

Introduction of non-uniform hypercoherence and multicoherence spaces.

Deterministic semantics with at most one vertex in intersections.

Abstract

In (hyper)coherence semantics, proofs/terms are cliques in (hyper)graphs. Intuitively, vertices represent results of computations and the edge relation witnesses the ability of being assembled into a same piece of data or a same (strongly) stable function, at arrow types. In (hyper)coherence semantics, the argument of a (strongly) stable functional is always a (strongly) stable function. As a consequence, comparatively to the relational semantics, where there is no edge relation, some vertices are missing. Recovering these vertices is essential for the purpose of reconstructing proofs/terms from their interpretations. It shall also be useful for the comparison with other semantics, like game semantics. In [BE01], Bucciarelli and Ehrhard introduced a so called non uniform coherence space semantics where no vertex is missing. By constructing the co-free exponential we set a new version of this last semantics, together with non uniform versions of hypercoherences and multicoherences, a new semantics where an edge is a finite multiset. Thanks to the co-free construction, these non uniform semantics are deterministic in the sense that the intersection of a clique and of an anti-clique contains at most one vertex, a result of interaction, and extensionally collapse onto the corresponding uniform semantics.