Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators

TL;DR

This paper investigates observational equivalences in symmetric interaction combinators, establishing full abstraction results by interpreting nets as edifices akin to Boehm trees, thus advancing the understanding of their computational semantics.

Contribution

It introduces two observational equivalences for symmetric interaction combinators and proves full abstraction for both, using a novel interpretation via edifices similar to Boehm trees.

Findings

Proves full abstraction for normal form equivalence

Proves full abstraction for head normal form equivalence

Interprets nets as edifices in the Cantor space

Abstract

The symmetric interaction combinators are an equally expressive variant of Lafont's interaction combinators. They are a graph-rewriting model of deterministic computation. We define two notions of observational equivalence for them, analogous to normal form and head normal form equivalence in the lambda-calculus. Then, we prove a full abstraction result for each of the two equivalences. This is obtained by interpreting nets as certain subsets of the Cantor space, called edifices, which play the same role as Boehm trees in the theory of the lambda-calculus.