Abstract:
We study two encodings of the asynchronous 
-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.
-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.Available as PostScript, PDF, DVI.