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

[Luca]

Dear Francesco,

a proof can be found in " Lazy Logical Semantics "  by Paolini, Ronchi 
https://urldefense.com/v3/__https://doi.org/10.1016/j.entcs.2004.10.003__;!!IBzWLUs!V2rFLTjuqLZZfc2Z5N5JuPtHkVE2P4_quDDG8lz9dwgyXX--cCQM7xTNkTtdXZqJpnyyVbrmEn7fj8mSP1357RaACt7BU0w$  
<https://urldefense.com/v3/__https://doi.org/10.1016/j.entcs.2004.10.003__;!!IBzWLUs!V2rFLTjuqLZZfc2Z5N5JuPtHkVE2P4_quDDG8lz9dwgyXX--cCQM7xTNkTtdXZqJpnyyVbrmEn7fj8mSP1357RaACt7BU0w$ >
  following the Berry proof (we considered both cbv/cbn).
  A  generalized  proof  can be found in   " Parametric λ -theories "  
by Luca Paolini, 2008,
https://urldefense.com/v3/__https://doi.org/10.1016/j.tcs.2008.01.021__;!!IBzWLUs!V2rFLTjuqLZZfc2Z5N5JuPtHkVE2P4_quDDG8lz9dwgyXX--cCQM7xTNkTtdXZqJpnyyVbrmEn7fj8mSP1357RaA25QNDjw$  
<https://urldefense.com/v3/__https://doi.org/10.1016/j.tcs.2008.01.021__;!!IBzWLUs!V2rFLTjuqLZZfc2Z5N5JuPtHkVE2P4_quDDG8lz9dwgyXX--cCQM7xTNkTtdXZqJpnyyVbrmEn7fj8mSP1357RaA25QNDjw$ >

Best,
Luca Paolini


On 03/04/23 14:56, Francesco Gavazzo wrote:
> [ 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