The Benefit of Being Non-Lazy in Probabilistic λ-calculus: Applicative Bisimulation is Fully Abstract for Non-Lazy Probabilistic Call-by-Name

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 [7] but not in lazy cbn [17].

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 [20], 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.