[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Paul, Thank you very much for the reply. To the best of my understanding, the CIU theorem refers to evaluation (or reduction) contexts, rather than applicative ones. I will check the proof of the CIU theorem anyway (perhaps the proof can be massaged to deal with applicative contexts only, assuming purity of the language). Thanks again, Francesco Il giorno mer 24 mag 2023 alle ore 11:36 Paul Levy <[email protected]> ha scritto: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Dear Francesco, > This is the “U” part of the so-called CIU theorem, due to Mason and > Talcott. It seems to be a fundamental result, as versions of it hold in > many different settings, including languages with local state and > nondeterminism. Soren Lassen’s thesis gives a good account in a > nondeterministic setting: > > https://urldefense.com/v3/__https://www.brics.dk/DS/98/2/BRICS-DS-98-2.pdf__;!!IBzWLUs!UrVwMt1-NZjJ9iyNJANkWYWHpY9-g9Ei6po0wyxnKTlmN920huODGRYEz1_ZGVbJO2y2IRgkg5LJhXMLg8hqyrrQDmUptTqL$ > Best wishes, > Paul > > > From: Types-list <[email protected]> on behalf of > Francesco Gavazzo <[email protected]> > Date: Friday, 19 May 2023 at 10:57 > To: Types list <[email protected]> > Subject: [TYPES] Full abstraction of applicative contexts in call-by-value > CAUTION: This email originated from outside the organisation. Do not click > links or open attachments unless you recognise the sender and know the > content is safe. > > > [ 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 >
