[Prev][Next][Index][Thread]
contextual full abstraction
Date: Fri, 1 Apr 88 12:50:57 BST
From: allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp (Allen Stoughton)>
To: meyer <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:meyer@theory.lcs.mit.edu>
Subject: Apt-Plotkin paper and full abstraction
Albert,
I don't have any results about whether the Apt-Plotkin model is not
contextually fully abstract. I did tell you that Mulmuley constructed
a model of the combinatory logic version of PCF that was fully
abstract but not contextually fully abstract. (This is before he
removed the top elements to get Milner's unique extensional f.a.
model.) A sufficient condition for a f.a. model to be contextually
f.a. is for it to be "inductively reachable" in the sense that all
elements can be reached by starting with the denotable elements and
closing under directed lubs for as long as it takes. (So
omega-algebraic and all finite elements definable implies inductively
reachable, but the converse is false; Also the least inductive
subalgebra of a f.a. model is thus contextually f.a.) But lack of
inductive reachability doesn't imply lack of contextual f.a....
Do you actually have a pair of contexts in mind that are operationally
equivalent when filled with abitrary terms in all contexts but
interpreted differently in their model?
Allen
------------------
Date: Fri, 1 Apr 88 14:40:28 EST
From: meyer
To: allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp>
In-reply-to: allen's message of Fri, 1 Apr 88 12:50:57 BST <8804011150.AA09336@sun.uucp>
Subject: Apt-Plotkin paper and full abstraction
Thanks for clarification. Seems I confused what you told me about the
failure of contextual f.a. in Mulmuley's setup with the non-statement of it
by Apt-Plotkin. No I didn't have a particular pair of contexts in
mind---I was just noticing the naive a priori possibility that they exist.
Thinking about it more, especially given that A-P allow ANY TOTAL
nondeterministc state transforms as denotations of constants, it wouldn't
surprise me if their semantics was c.f.a. for program contexts with program
holes, but I don't have time to think it through now.
Is it ok to forward this correspondence to the TYPES and LOGIC lists?
Regards, A.
---------
Date: Sat, 2 Apr 88 12:29:27 BST
From: allen <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:allen@csta.uucp (Allen Stoughton)>
To: meyer <@NSS.Cs.Ucl.AC.UK,@cvaxa.sussex.ac.uk:meyer@theory.lcs.mit.edu>
Subject: Re: Apt-Plotkin paper and full abstraction
Yes, it's fine to forward my response to the lists.
Allen