2026-08-14T17:25:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10533 2024-03-06T10:46:09Z ddc:004 open_access

The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus Kašterović, Simona Pagani, Michele probabilistic lambda calculus bisimulation Howe’s technique context equivalence testing We consider the notion of probabilistic applicative bisimilarity (PAB), recently introduced as a behavioural equivalence over a probabilistic extension of the untyped lambda-calculus. Alberti, Dal Lago and Sangiorgi have shown that PAB is not fully abstract with respect to the context equivalence induced by the lazy call-by-name evaluation strategy. We prove that extending this calculus with a let-in operator allows for achieving the full abstraction. In particular, we recall Larsen and Skou’s testing language, which is known to correspond with PAB, and we prove that every test is representable by a context of our calculus. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Simona Kašterović and Michele Pagani 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.26 urn:nbn:de:0030-drops-105338 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.26 eng https://creativecommons.org/licenses/by/3.0/legalcode