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.