Full Abstraction for Set-Based Models of the Symmetric Interaction Combinators

The symmetric interaction combinators are a model of distributed
and deterministic computation based on Lafont’s interaction
nets, a special form of graph rewriting. The interest of the symmetric interaction
combinators lies in their universality, that is, the fact that they
may encode all other interaction net systems; for instance, several implementations
of the lambda-calculus in the symmetric interaction combinators
exist, related to Lamping’s sharing graphs for optimal reduction.
A certain number of observational equivalences were introduced for this
system, by Lafont, Fernandez and Mackie, and the first author. In this
paper, we study the problem of full abstraction with respect to one of
these equivalences, using a class of very simple denotational models based
on pointed sets.