Hostname: page-component-8448b6f56d-dnltx Total loading time: 0 Render date: 2024-04-19T23:35:45.672Z Has data issue: false hasContentIssue false
  • English
  • Français

Non-uniform (hyper/multi)coherence spaces

Published online by Cambridge University Press:  01 November 2010

PIERRE BOUDES
PIERRE BOUDES*
Affiliation:
Laboratoire d'Informatique de Paris Nord (UMR 7030), CNRS/université Paris nord, institut Galilée, 99 av. J.-B. Clément, 93430 Villetaneuse, France Email: boudes@univ-paris13.fr
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

In (hyper)coherence semantics, 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.

Bucciarelli and Ehrhard (2001) 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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 21 , Issue 1 , February 2011 , pp. 1 - 40
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S., Jagadeesan, R. and Malacaria, P. (1994) Full abstraction for PCF. In: Hagiya, M. and Mitchell, J. C. (eds.) Theoretical Aspects of Computer Software, Springer-Verlag 1–15.Google Scholar
Amadio, R. M. and Curien, P.-L. (1998) Domains and lambda-calculi, Cambridge Tracts in Theoretical Computer Science 46, Cambridge University Press.CrossRefGoogle Scholar
Barreiro, N. and Ehrhard, T. (1997) Anatomy of an extensional collapse. Available by ftp from iml.univ-mrs.fr/pub/ehrhard/.Google Scholar
Berry, G. and Curien, P.-L. (1982) Sequential algorithms on concrete data structures. Theoretical Computer Science 20 265–321.CrossRefGoogle Scholar
Bierman, G. M. (1995) What is a categorical model of intuitionistic linear logic? In: Dezani, M. (ed.) Proceedings of Conference on Typed lambda calculus and Applications. Springer-Verlag Lecture Notes in Computer Science 902.Google Scholar
Boudes, P. (2003) Non-uniform hypercoherences. In: Blute, R. and Selinger, P. (eds.) Proceedings of CTCS 2002. Electronic Notes in Theoretical Computer Science 69.CrossRefGoogle Scholar
Boudes, P. (2004) Projecting games on hypercoherences. In: Proceedings of ICALP. Springer-Verlag Lecture Notes in Computer Science 3142 257–268.CrossRefGoogle Scholar
Boudes, P. (2005) Desequentialization of games and experiments in proof-nets. Pré-publication IML 2005-1.Google Scholar
Bruasse-Bac, A. (2001) Logique linéaire indexée du second ordre, Ph.D. thesis, Université Aix-Marseille II – Méditerranée.Google Scholar
Bucciarelli, A. and Ehrhard, T. (1994) Sequentiality in an extensional framework. Information and Computation 110 (2).CrossRefGoogle Scholar
Bucciarelli, A. and Ehrhard, T. (2000) On phase semantics and denotational semantics in multiplicative-additive linear logic. APAL 102 (3)247–282.Google Scholar
Bucciarelli, A. and Ehrhard, T. (2001) On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic 109 (3)205–241.CrossRefGoogle Scholar
Cartwright, R., Curien, P.-L. and Felleisen, M. (1994) Fully abstract semantics for observably sequential languages. Information and Computation 111 (2)297–401.CrossRefGoogle Scholar
Ehrhard, T. (1993) Hypercoherences: a strongly stable model of linear logic. Mathematical Structures in Computer Science 3 365–385.CrossRefGoogle Scholar
Ehrhard, T. (1999) A relative definability result for strongly stable functions and some corollaries. Information and Computation 152.CrossRefGoogle Scholar
Ehrhard, T. (2000) Parallel and serial hypercoherences. Theoretical computer science 247 39–81.CrossRefGoogle Scholar
Ehrhard, T. (2004) A completeness theorem for symmetric product phase spaces. J. Symb. Log. 69 (2)340–370.CrossRefGoogle Scholar
Ehrhard, T. (2005) Finiteness spaces. Mathematical Structures in Computer Science 15 (4)615–646.CrossRefGoogle Scholar
Girard, J.-Y. (1987) Linear logic. Theoretical Computer Science 50 1–102.CrossRefGoogle Scholar
Girard, J.-Y. (1996) On denotational completeness (manuscript).CrossRefGoogle Scholar
Girard, J.-Y. (2001) Locus Solum. Mathematical Structures in Computer Science 11 (3)301–506.CrossRefGoogle Scholar
Longley, J. (2002) The sequentially realizable functionals. Annals of Pure and Applied Logic 117 (1-3)1–93.CrossRefGoogle Scholar
Melliès, P.-A. (2004) Comparing hierarchies of types in models of linear logic. Information and Computation 189 (2)202–234.CrossRefGoogle Scholar
Melliès, P.-A. (2005) Sequential algorithms and strongly stable functions. Theoretical Computer Science 343 (1-2)237–281.CrossRefGoogle Scholar
Pagani, M. (2006) Acyclicity and coherence in multiplicative exponential linear logic. In: Ésik, Z. (ed.) Proceedings 15th EACSL Annual Conference on Computer Science Logic (CSL'06). Springer-Verlag Lecture Notes in Computer Science 4207 531–545.CrossRefGoogle Scholar
Tortora de Falco, L. (2000) Réseaux, cohérence et expériences obsessionnelles, Thèse de doctorat, Université Paris VII.Google Scholar
van Oosten, J. (1997) A combinatory algebra for sequential functionals of finite type. Technical Report 996, University of Utrecht.Google Scholar