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

[Francesco Gavazzo]

Dear Sergey,

Thank you very much for the reply. I see your point, although I am not
fully convinced about it. In fact, the description of applicative
similarity by Abramsky you mentioned seems not that innocent to me: it
states that applicative similarity as defined coinductively relying on
Knaster-Tarski Theorem can be stratified in a finitary way, hence relying
on  Kleene Theorem (such a characterisation usually requires cocontinuity
of the defining functional of simulation, which does not hold in general --
such as in presence of effects).

The proof of compatibility of applicative similarity by Howe’s method
relies on the coinductive characterisation of applicative similarity, hence
taking no advantage of the aforementioned stratification --- which,
instead, gives the inclusion of contextual approximation in applicative
similarity. This is one of the reasons for the robustness of Howe’s method.
What Ugo and I were wondering is whether it is possible to take advantage
of stratification to give a somehow elementary proof of compatibility of
stratified similarity. This is in line with Berry’s proof of the context
lemma which, to the best of my knowledge, has been adapted to the case of
(lazy) CbN, but not CbV (hence our question on Types).

This question comes from some work Ugo and I are doing on testing
equivalence for higher-order languages. In that context (especially working
with nondeterministic languages), we observed that (mild variations of)
stratifications of applicative similarity seem to always be fully abstract.
The crucial point behind that is precisely the finitary definition of
stratified applicative preorders, something that contrasts with the deeply
infinitary nature of applicative similarity.

Thanks again for your reply and all the best,
Francesco (and Ugo)

Il giorno ven 19 mag 2023 alle ore 13:25 Sergey Goncharov <sergyy at gmail.com>
ha scritto:

> 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!VMxR19aOmk8H4US6MYYKj9PxKCGtUohdiFXKEAjP4wnekxa2q00J24HDNlxxNhDrJkiL1gJvIMwSy2pnh_tTGS2n9TeBHsvI0OWADA$ ) 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
>