Damiano Mazza - Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators

lmcs:1150 - Logical Methods in Computer Science, December 22, 2009, Volume 5, Issue 4 - https://doi.org/10.2168/LMCS-5(4:6)2009
Observational Equivalence and Full Abstraction in the Symmetric Interaction CombinatorsArticle

Authors: Damiano Mazza

    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.


    Volume: Volume 5, Issue 4
    Published on: December 22, 2009
    Imported on: February 29, 2008
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Discrete Mathematics,F.3.2,F.4.1

    2 Documents citing this article

    Consultation statistics

    This page has been seen 979 times.
    This article's PDF has been downloaded 428 times.