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

[Sergey Goncharov]

Dear Francesco,

to me, the overhead behind the indicated consequence seems to be essentially the same as behind the 
claim that applicative bisimilarity coincides with the contextual equivalence.

In the original paper by Abramsky (https://urldefense.com/v3/__https://www.cs.ox.ac.uk/files/293/lazy.pdf__;!!IBzWLUs!SZc2ydLt6rmd0OC15QUW3eaZwMZAjQAuonkDOCvbZpGEihVz8lCRLFEA1RZ832wm220NZHGw6WriSRynZw64v-0fAQ$ ) he provides in Definition 
2.3 an equivalent description of the applicative simulation preorder, which can be easily adapted to the 
call-by-value setting. From that definition we see that t would be applicative-smaller-or-equal to s iff 
for any values v1, ... , vn if (t v1 ... vn) terminates then (s v1 ... vn) terminates. This is exactly 
the definition of the contextual preorder wrt the restricted class of contexts you describe.

Cheers,
Sergey

> 
> 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