Hostname: page-component-78c5997874-lj6df Total loading time: 0 Render date: 2024-11-06T13:07:54.842Z Has data issue: false hasContentIssue false
  • English
  • Français

A denotational semantics for the symmetric interaction combinators

Published online by Cambridge University Press:  01 June 2007

DAMIANO MAZZA
DAMIANO MAZZA*
Affiliation:
Institut de Mathématiques de Luminy (UMR 6206), Campus de Luminy, Case 907 – 13288 Marseille Cedex 9, France Email: [email protected] Website: http://iml.univ-mrs.fr/~mazza.
Get access Rights & Permissions [Opens in a new window]

Abstract

The symmetric interaction combinators are a variant of Lafont's interaction combinators. They enjoy a weaker universality property with respect to interaction nets, but are equally expressive. They are a model of deterministic distributed computation and share the good properties of Turing machines (elementary reductions) and of the λ-calculus (higher-order functions and parallel execution). We introduce a denotational semantics for this system, which is inspired by the relational semantics for linear logic, and prove an injectivity and full completeness result for it. We also consider the algebraic semantics defined by Lafont, and prove that the two are strongly related.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 17 , Issue 3 , June 2007 , pp. 527 - 562
Copyright
Copyright © Cambridge University Press 2007

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

Danos, V. and Regnier, L. (1989) The structure of multiplicatives. Archive for Mathematical Logic 28 181–203.CrossRefGoogle Scholar
Ehrhard, T. (2005) Finiteness spaces. Mathematical Structures in Computer Science 15 (4)615–646.CrossRefGoogle Scholar
Fernández, M. and Mackie, I. (2003) Operational equivalence for interaction nets. Theoretical Computer Science 297 (1–3) 157–181.CrossRefGoogle Scholar
Girard, J.-Y. (1987a) Linear logic. Theoretical Computer Science 50 (1)1–102.CrossRefGoogle Scholar
Girard, J.-Y. (1987b) Multiplicatives. In: Lolli, G. (ed.) Logic and Computer Science: New Trends and Applications, Rendiconti del Seminario Matematico dell'Università e Politecnico di Torino 11–34.Google Scholar
Girard, J.-Y. (1989) Geometry of interaction I: interpretation of System F. In: Proceedings of the Logic Colloquium '88, North Holland 221–260.CrossRefGoogle Scholar
Gonthier, G., Abadi, M. and Lévy, J.-J. (1992) The geometry of optimal lambda reduction. In: Conference Record of the Nineteenth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 92), ACM Press 15–26.Google Scholar
Lafont, Y. (1990) Interaction nets. In: Conference Record of POPL'90, ACM Press 95–108.CrossRefGoogle Scholar
Lafont, Y. (1995) From proof nets to interaction nets. In: Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic, Cambridge University Press 225–247.CrossRefGoogle Scholar
Lafont, Y. (1997) Interaction combinators. Information and Computation 137 (1)69–101.CrossRefGoogle Scholar
Lippi, S. (2002) Encoding left reduction in the lambda-calculus with interaction nets. Mathematical Structures in Computer Science 12 (6)797–822.CrossRefGoogle Scholar
Mackie, I. and Pinto, J. S. (2002) Encoding linear logic with interaction combinators. Information and Computation 176 (2)153–186.CrossRefGoogle Scholar
Mazza, D. (2006) Observational equivalence for the interaction combinators and internal separation. In: Mackie, I. (ed.) Proceedings of TERMGRAPH 2006. Electronic Notes in Theoretical Computer Science 7–16.Google Scholar
Pagani, M. (2007) Proofs, denotational semantics and observational equivalence in Multiplicative Linear Logic. Mathematical Structures in Computer Science 17 (2)341–359.CrossRefGoogle Scholar