[Prev][Next][Index][Thread]
Stability and Sequentiality
Below some recent email between Jim/Meyer, Berry, and Curien on the topic.
It seems Sieber's ``logical relations'' method for paring down
Scott-continuous models offers a general method similar in spirit to the
specific ``extensional compatibility'' repair Berry suggests below for avoiding
the counterexamples we note.
------------
---------
Date: Wed, 10 May 89 18:42:57 EDT
From: trevor@theory.LCS.MIT.EDU
To: curien@src.dec.com, jlevy@src.dec.com,
mcvax!inria.inria.fr!jlevy@uunet.uu.net,
mcvax!inria.inria.fr!levy@uunet.uu.net,
mcvax!mirsa.inria.fr!berry@uunet.uu.net, meyer@theory.LCS.MIT.EDU
Recently we have been looking at models of PCF, in particular at the
very interesting stable function and also extensional sequential
algorithm models which you have developed. It was neat to see how
these models restored the validity of Plotkin's counter-example to
full abstraction of Scott Domains for PCF.
But we were surprised to finally realize that the sense in which these
models meet the stated goal of your "State of the Art" paper--to be
"closer" to the fully abstract model of PCF--has not been clearly
achieved. Namely, even though Plotkin's equation, which fails in the
Scott model, does indeed hold in the stable model, OTHER equations
which DO hold in the Scott model, fail in the stable model.
It doesn't seem fair to call the stable model "closer" than the Scott
model, since the equational theories of the two models are
set-theoretically incomparable. This kind of incomparability appears
to hold for any pair of the the four models under consideration: Scott
Domains, dcds's, stable models, and extensional sequential
algorithms--though we haven't checked this.
Are we missing some deeper sense in which one of these models is
closer to full abstraction for PCF than the others? Are we correct in
presuming all the theories are incomparable?
The example where stable models do worse than Scott domains is one we
presume you're aware of since it is pointed out in Curien's monograph: in
the continous model, left-strict OR (LSOR) and right-strict OR (RSOR) are
bounded above by POR. However POR does not exist in the stable model,
which is why Plotkin's counter-example gets fixed. But the penalty for
this fix is that without POR, a ``separator'' function returning TRUE on
LSOR and FALSE on RSOR makes perfect sense, i.e., it is continuous in the
stable model, but does not exist [...] in the Scott model.
This leads to an equation holding in the continuous model which does not
hold in the stable model. Let
M_i = \f. if (f LSOR) (if (not(f RSOR)) i omega) omega
M_i is thus the functional which tests if its argument is a LSOR/RSOR
separator, returning i if so, and diverging otherwise. Then in the
Scott model M_0 = M_1 because both terms denote the constant divergent
function, but the equation fails in the stable model because the
separator exists.
Look forward to hearing from you on this.
Regards, Albert and Trevor Jim
------------
---------------
Date: Sun, 14 May 89 22:25:43 +0200
From: Gerard Berry <Gerard.Berry@mirsa.inria.fr>
To: berry@mirsa.inria.fr, curien@margaux.inria.fr, meyer@theory.LCS.MIT.EDU,
trevor@theory.LCS.MIT.EDU
Hi!
Thanks for your letter! I am happy to see you interested in stable
functions! The pity is that I never wrote a specific stable function
paper in publishable form. At those old times (79), nobody seemed
to care very much... It is quite up in my pile now.
I think I can partly answer your question. The "pure" single-ordered stable
model is of course quite different from the Scott one, and even the
identity and the constant function top can be discriminated in {bottom,top}.
This is precisely why I introduced the bi-ordered model that seemed to
keep both aspects of Scott continuity and stability. But, as you point
out, there are still difficulties with this finer model, and your counter-
example exhibits one. Indeed, my statement that the biordered stable
model is "closer" to the fully abstract one is informal and is not OK with
the definition I give of bidomains. Here is a change to the definition
that solves your counter-example. It is based on the remark that
compatibility cannot any more be defined by existence of lubs, but must be
axiomatized on its own.
Add to bicpos and bidomains an "extensional compatibility" relation
COMP such that (< being the extensional ordering)
if x<y then x COMP y
if x<y, x'<y', y COMP y', then x COMP x'
for DELTA, DELTA' directed, if for all x in DELTA and y in DELTA'
one has x COMP y, then lub DELTA COMP lub DELTA'
Now, require functions to preserve COMP, that is f(x) COMP f(y) if
x COMP y. Define f COMP g iff f(x) COMP g(y) when x COMP y.
Then exponentiation goes through (as far as I can see without working too
hard), and your discriminator disappears.
I don't know how far this goes. I agree one should compare the induced
relations on terms, which I didn't do. Do you know how to do it?
Regards, Gerard
---------------
--------------------
From: curien@src.dec.com (Pierre-Louis Curien)
Date: 15 May 1989 1029-PDT (Monday)
To: trevor@theory.LCS.MIT.EDU, meyer@theory.LCS.MIT.EDU
Cc: berry@mirsa.inria.fr
Fcc: outbox
Subject: Re:
In-Reply-To: Your message of Wed, 10 May 89 18:42:57 EDT
<8905102242.AA00444@albatross.LCS.MIT.EDU>
Dear Trevor, Albert (and Gerard).
I had the occasion to read your message in peace on the plane to
Houston, where I visited the PL group at Rice U.
1) Like Gerard, I never looked at the induced theories, but it is an
interesting point of view.
2) I think that Gerard had a result in his thesis of the kind: the
fully abstract model of PCF, as constructed a la Milner by quotient
and limit, is made of stable functions, and I kind of remember that
it was the main reason for claiming the stable model to be "closer"
to full abstraction (Gerard: true?)
3) Your counter-example for showing that the stable model can
discriminate terms where the continuous did not is very similar in
spirit to the examples I exhibit in the last section of my monograph
(4.4), to show that the extensional sequential model is *not* fully
abstract. And indeed, it might be the case, (although I did not check
this) that my counter-examples have a similar status of *not* being
ones in the continuous model.
And indeed the kind of treatment that Gerard suggests is very similar
to the treatment I had tried to give (not in my book, where the
only track of this effort is an "exercise" (the first p.272),
but in my thesis) to get rid of those counter examples. But you imagine
that when you have two orders and a funny compatibility to carry around,
you must be a very good acrobat...
Please let me know your further investigations in the subject.
Pierre-Louis