Bisimilarity vs. Observational Equivalence
Apr. 9th, 2013 08:00 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codedotOperational equivalence for interaction nets
Maribel Fernández, Ian Mackie
The notion of contextual (or operational) equivalence is fundamental in the theory of programming languages. By setting up a notion of bisimilarity, and showing that it coincides with contextual equivalence, one obtains a simple coinductive proof technique for showing that two programs are equivalent in all contexts. In this paper we apply these (now standard) techniques to interactions nets, a graphical programming language characterized by local reduction. This work generalizes previous studies of operational equivalence in typed interaction nets since it can be applied to untyped systems, thus all systems of interaction nets are captured.
http://www.sciencedirect.com/science/article/pii/S0304397502006370
Observational Equivalence for the Interaction Combinators and Internal Separation
Damiano Mazza
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öhm's Theorem for the λ-calculus.
http://www.sciencedirect.com/science/article/pii/S1571066107001880
Maribel Fernández, Ian Mackie
The notion of contextual (or operational) equivalence is fundamental in the theory of programming languages. By setting up a notion of bisimilarity, and showing that it coincides with contextual equivalence, one obtains a simple coinductive proof technique for showing that two programs are equivalent in all contexts. In this paper we apply these (now standard) techniques to interactions nets, a graphical programming language characterized by local reduction. This work generalizes previous studies of operational equivalence in typed interaction nets since it can be applied to untyped systems, thus all systems of interaction nets are captured.
http://www.sciencedirect.com/science/article/pii/S0304397502006370
Observational Equivalence for the Interaction Combinators and Internal Separation
Damiano Mazza
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öhm's Theorem for the λ-calculus.
http://www.sciencedirect.com/science/article/pii/S1571066107001880
