Abstract:
We consider the probabilistic applicative bisimilarity (PAB) --- a coinductive relation comparing the applicative behaviour of probabilistic untyped λ-terms according to a specific operational semantics. This notion has been studied by Dal Lago et al. with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body of a function. In particular, PAB has been proven to be fully abstract with respect to the contextual equivalence in cbv [6] but not in lazy cbn [16].
We overcome this issue of cbn by relaxing the laziness constraint: we prove that PAB is fully abstract with respect to the standard head reduction contextual equivalence. Our proof is based on Leventis' Separation Theorem [19], using probabilistic Nakajima trees as a tree-like representation of the contextual equivalence classes.
Finally, we prove also that the inequality full abstraction fails, showing that the probabilistic applicative similarity is strictly contained in the contextual preorder.
