The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.26
URN: urn:nbn:de:0030-drops-105338
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10533/
Go to the corresponding LIPIcs Volume Portal

Kasterovic, Simona ; Pagani, Michele

The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus

pdf-format:
LIPIcs-FSCD-2019-26.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{kasterovic_et_al:LIPIcs:2019:10533,
  author =	{Simona Kasterovic and Michele Pagani},
  title =	{{The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10533},
  URN =		{urn:nbn:de:0030-drops-105338},
  doi =		{10.4230/LIPIcs.FSCD.2019.26},
  annote =	{Keywords: probabilistic lambda calculus, bisimulation, Howe's technique, context equivalence, testing}
}

Keywords: probabilistic lambda calculus, bisimulation, Howe's technique, context equivalence, testing
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI