History


Please fill in your query. A complete syntax description you will find on the General Help page.
Non-uniform (hyper/multi)coherence spaces. (English)
Math. Struct. Comput. Sci. 21, No. 1, 1-40 (2011).
Summary: In (hyper)coherence semantics, proofs/terms are cliques in (hyper)graphs. Intuitively, the vertices represent the results of computations and the edge relation witnesses the ability to carry out the computation assembled into a single piece of data or a single (strongly) stable function, at arrow types. Also, the argument of a (strongly) stable functional is always a (strongly) stable function. As a consequence, compared to the relational semantics where there is no edge relation, some vertices are missing. Recovering these vertices is essential if we are to reconstruct proofs/terms from their interpretations. It will also be useful for comparing with other semantics, such as game semantics. In [Ann. Pure Appl. Logic 109, No. 3, 205‒241 (2001; Zbl 1004.03051)], {\it A. Bucciarelli} and {\it T. Ehrhard} introduced a non-uniform coherence space semantics, where no vertex is missing. By constructing the co-free exponential, we get a new version of this semantics, together with non-uniform versions of hypercoherences and multicoherences. This provides a new semantics in which 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 an anti-clique contains at most one vertex, which is a result of interaction, and they then extensionally collapse onto the corresponding uniform semantics.
WorldCat.org
Valid XHTML 1.0 Transitional Valid CSS!