[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Francesco, This is the “U” part of the so-called CIU theorem, due to Mason and Talcott. It seems to be a fundamental result, as versions of it hold in many different settings, including languages with local state and nondeterminism. Soren Lassen’s thesis gives a good account in a nondeterministic setting: https://urldefense.com/v3/__https://www.brics.dk/DS/98/2/BRICS-DS-98-2.pdf__;!!IBzWLUs!UrVwMt1-NZjJ9iyNJANkWYWHpY9-g9Ei6po0wyxnKTlmN920huODGRYEz1_ZGVbJO2y2IRgkg5LJhXMLg8hqyrrQDmUptTqL$ Best wishes, Paul From: Types-list <[email protected]> on behalf of Francesco Gavazzo <[email protected]> Date: Friday, 19 May 2023 at 10:57 To: Types list <[email protected]> Subject: [TYPES] Full abstraction of applicative contexts in call-by-value CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe. [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Dear all, It is well-known that applicative bisimilarity is fully abstract on the untyped call-by-value λ-calculus. A direct consequence of that is that contextual equivalence can be restricted to applicative contexts (namely contexts defined by the grammar E ::= [-] | Ev) leaving its discriminated power unchanged. Such a result is, in principle, independent of applicative bisimilarity and I was wondering if any of you is aware of any direct (i.e. not going through applicative bisimilarity) proof that applicative contexts suffice to characterise contextual equivalence. Thanks a lot in advance! Best, Francesco Gavazzo and Ugo Dal Lago
