Open AccessDecoding Choice Encodings
Author(s) -
Uwe Nestmann,
Benjamin C. Pierce
Publication year - 1999
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v6i42.20112
Subject(s) - mathematical proof , correctness , atomicity , divergence (linguistics) , computer science , equivalence (formal languages) , asynchronous communication , encoding (memory) , branching (polymer chemistry) , decoding methods , theoretical computer science , process calculus , algorithm , mathematics , discrete mathematics , programming language , artificial intelligence , computer network , linguistics , philosophy , materials science , geometry , database transaction , composite material
We study two encodings of the asynchronous pi-calculus with input-guarded choice into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser - but still coinductively defined - equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit decodings from translations to source terms.