[TYPES] Full abstraction of applicative contexts in call-by-value

[Francesco Gavazzo]

Dear Paul,

Thank you very much for the reply. To the best of my understanding, the CIU
theorem refers to evaluation (or reduction) contexts, rather than
applicative ones.
I will check the proof of the CIU theorem anyway (perhaps the proof can be
massaged to deal with applicative contexts only, assuming purity of the
language).
Thanks again,
Francesco

Il giorno mer 24 mag 2023 alle ore 11:36 Paul Levy <p.b.levy at bham.ac.uk> ha
scritto:

> [ 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 <types-list-bounces at LISTS.SEAS.UPENN.EDU> on behalf of
> Francesco Gavazzo <francesco.gavazzo at gmail.com>
> Date: Friday, 19 May 2023 at 10:57
> To: Types list <types-list at lists.seas.upenn.edu>
> 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
>