Observational Equivalence for the Interaction Combinators and Internal Separation

We define an observational equivalence for Lafont’s interaction combinators, which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free normal form) respecting reduction. More interestingly, this equivalence enjoys an internal separation property similar to that of B¨ohm’s Theorem for the λ-calculus.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Damiano Mazza
• Keywords: Discriminating Non-trivial Congruence, ENTCS 2007, Lafont’s Interaction Combinators, Observational Equivalence