Observational Equivalence for the Interaction Combinators and Internal Separation

Damiano Mazza

doi:10.1016/j.entcs.2006.10.030

Observational Equivalence for the Interaction Combinators and Internal Separation

Damiano Mazza

Université de Provence

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

Abstract

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.

Original language	English
Pages (from-to)	113-137
Number of pages	25
Journal	Electronic Notes in Theoretical Computer Science
Volume	176
Issue number	1
DOIs	https://doi.org/10.1016/j.entcs.2006.10.030
Publication status	Published - 28 May 2007
Externally published	Yes

Keywords

Böhm's Theorem
Interaction nets
interaction combinators
internal separation
observational equivalence

Access to Document

10.1016/j.entcs.2006.10.030

Cite this

@article{f46e10e66a7b4694843207f629a98bcf,

title = "Observational Equivalence for the Interaction Combinators and Internal Separation",

abstract = "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{\"o}hm's Theorem for the λ-calculus.",

keywords = "B{\"o}hm's Theorem, Interaction nets, interaction combinators, internal separation, observational equivalence",

author = "Damiano Mazza",

year = "2007",

month = may,

day = "28",

doi = "10.1016/j.entcs.2006.10.030",

language = "English",

volume = "176",

pages = "113--137",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "1",

}

TY - JOUR

T1 - Observational Equivalence for the Interaction Combinators and Internal Separation

AU - Mazza, Damiano

PY - 2007/5/28

Y1 - 2007/5/28

N2 - 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.

AB - 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.

KW - Böhm's Theorem

KW - Interaction nets

KW - interaction combinators

KW - internal separation

KW - observational equivalence

U2 - 10.1016/j.entcs.2006.10.030

DO - 10.1016/j.entcs.2006.10.030

M3 - Article

AN - SCOPUS:34248530867

SN - 1571-0661

VL - 176

SP - 113

EP - 137

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 1

ER -

Observational Equivalence for the Interaction Combinators and Internal Separation

Abstract

Keywords

Access to Document

Fingerprint

Cite this