The Benefit of Being Non-Lazy in Probabilistic {\\lambda}-calculus

We consider the probabilistic applicative bisimilarity (PAB), a coinductive\nrelation comparing the applicative behaviour of probabilistic untyped lambda\nterms according to a specific operational semantics. This notion has been\nstudied with respect to the two standard parameter passing policies,\ncall-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not\nreducing within the body of a function. In particular, PAB has been proven to\nbe fully abstract with respect to the contextual equivalence in cbv but not in\nlazy cbn. We overcome this issue of cbn by relaxing the laziness constraint: we\nprove that PAB is fully abstract with respect to the standard head reduction\ncontextual equivalence. Our proof is based on the Leventis Separation Theorem,\nusing probabilistic Nakajima trees as a tree-like representation of the\ncontextual equivalence classes. Finally, we prove also that the inequality full\nabstraction fails, showing that the probabilistic applicative similarity is\nstrictly contained in the contextual preorder.\n

Paper

Similar papers

© 2026 NYSGPT2525 LLC