[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <ser...@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 >
