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