A Denotational Semantics for the Symmetric Interaction Combinators


Damiano Mazza

Mathematical Structures in Computer Science 17 (3)

Cambridge University Press


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, sharing the good properties of Turing machines (elementary reductions) and of the lambda-calculus (higher-order functions, parallel execution). We introduce a denotational semantics for this system, inspired by the relational semantics for linear logic, proving 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.

Download: CombSemantics.pdf