[Prev][Next][Index][Thread]
Sieber's Full-Abstraction for call-by-value (241 lines)
Date: Sun, 30 Jul 89 00:20:14 CDT
To: sieber%fb10vax.informatik.uni-saarland.dbp.de@relay.cs.net
Cc: meyer@theory.LCS.MIT.EDU, plotkin@src.dec.com, dorai@titan.rice.edu
In-Reply-To: meyer@theory.lcs.mit.edu's message of Fri, 28 Jul 89 15:31:53 EDT
Kurt: I have a comment and two technical questions on your part in the
message that Albert posted on types.
Part 1:
=======
A student of mine and I have worked on call-by-value LCF this summer
and we reproved a similar result (as a building block for models of
control, side-effects, etc. in cbv languages). The major difference
is in our model is the construction of the arrow domains, which are
lifted strict function spaces. In other words,
i denotes N_bot (domain of pos ints)
o denotes T_bot (domain of truth values)
s ->t denotes [D_s --->_strict D_t]_bot
[We believe that this is more in synch w/ traditional denotational
semantics where every domain conatins a bottom element for denoting
diverging computations on that domain. Your approach is closer in
spirit to Eugenio's monad approach. Our model leads to the same
notational overhead as your model; I realized that while talking to
Gordon two weeks ago.]
Unlike in your model, we have the constant-undefined function as a
finite step function. Although this seems to be the only difference,
it seems to avoid the first technical problem that you mention:
<> there is only ONE constant function per strict function domain,
namely, {(x,bot) | x in D}
<> and this is a finite function: [bot ==>s bot].
[ ==>s are strict one-step functions.]
Your second techical problem:
>
> - a finite element f of type (s1->...->sn->t), t ground type, is NOT
> necessarily the lub of threshold functions of the form
> (d1=>...=>dn=>e), because some of the threshold functions might be
> "shorter", i.e. of the form (d1=>..=>dm=>\x.bottom) where m<n.
doesn't seem to come up for us (perhaps because of the above
difference between our approachs?) and I can't seem to verify it for
your model. It appears to me that you only need (and could) to show
conditions (1) and (2) on page 239 of [Plotkin], and this suffices for
Lemma 4.5.
Question: What am I overlooking?
Part 2:
=======
Unlike you, we also proved an adequacy result that connects the
operational semantics of cbv-lambda [Plotkin75:TCS1] w/ the
denotational semantics. [I know this is superfluous, but again, we
have generalizations in mind where it may not be as obvious.]
We first tried to adapt Plotkin's technique by modifying the Comp(s)
relation, but we failed. We went back to a "direct" proof which is
less elegant (but works).
Question: Did you try to prove Thm 3.1 by modifying the Comp relation
(and, if so, how did you modify it)?
Thanks and regards -- Matthias
-------------------------------------------
Date: 31 Jul 89 13:58 GMT-0100
From: Kurt Sieber <sieber%fb10vax.informatik.uni-saarland.dbp.de@relay.cs.net>
To: matthias%rice.edu%eansb.uucp@relay.cs.net
Cc: meyer%theory.lcs.mit.edu%eansb.uucp@relay.cs.net,
plotkin%src.dec.com%eansb.uucp@relay.cs.net,
dorai%titan.rice.edu%eansb.uucp@relay.cs.net
In-Reply-To: <Matthias Felleisen's message of Sun, 30 Jul 89 13:49:59 +0200 (MET dst) <<8907300520.AA07355@titan.rice.edu>>.de>
Subject: full-abstraction for call-by-value
Date: Mon, 31 Jul 89 14:57:52 +0200 (MET dst)
1) Models:
The relation between your model and my model is as follows:
Your D^t is isomorphic (as a cpo) to my D^t_bottom
(Proof by induction on types)
In Moggi's terminology:
I have defined the VALUES of type t and you have defined the
COMPUTATIONS of type t. That's why I suggest the following
notation (accepting Gordon's nomenclature):
- V^t = the dcpo of values of type t (= my D^t)
- C^t = the dcppo of computations of type t (= your D^t = V^t_bottom)
2) Constant functions:
I only claimed that for each d in V^t (i.e. d NOT bottom) the
constant function
\x:s.d : V^s --> C^t
is not finite. This also holds in your model; a source of
confusion is, that you consider it as a strict function in
C^s --> C^t
hence it's no longer CONSTANT. That's why you obtain the funny
result that \x:s.bottom is the only constant function.
3) Short threshold functions:
I can't see why this problem should disappear in your approach.
Consider the (finite) function
f = (0 => \x:i.bottom)
of type (i -> i -> i), i.e. f n TERMINATES for n = 0 (with
result \x:i.bottom) and diverges for n > 0. How can f be the lub
of threshold functions of "length" 3 ?
4) Computational adequacy:
I haven't thought about it at all, but that doesn't mean that I
consider it as superfluous. Albert told me that Gordon has proved
it before, but that he needed an "unnatural" operational semantics.
Perhaps I've misunderstood Albert; in any case it seems that there
is also some confusion about computational adequacy.
Regards
Kurt.
------------------------------
Date: 31 Jul 89 14:59 GMT-0100
From: Kurt Sieber <sieber%fb10vax.informatik.uni-saarland.dbp.de@relay.cs.net>
To: plotkin%src.dec.com%eansb.uucp@relay.cs.net
Cc: meyer%theory.lcs.mit.edu%eansb.uucp@relay.cs.net,
matthias%rice.edu%eansb.uucp@relay.cs.net
Subject: full abstraction for call-by-value
Date: Mon, 31 Jul 89 15:59:21 +0200 (MET dst)
Dear Gordon.
1) I still don't understand the difference between
- (your) partial continuous functions from D to E and
- (my) continuous functions from D to E_bottom.
Note that I have NOT used strict functions from D_bottom to
E_bottom, because I agree with you that first adding bottom to D
and then taking it out via strictness is at least odd, if not
misleading.
Actually I like Moggi's terminology:
bottom is NOT a value (i.e. it cannot be assigned to a variable),
but it IS a computation (i.e. it can occur as the meaning of a
lambda term).
Hence the question is not WHETHER to use bottom, but WHERE to use
it.
Do you agree ?
2) I agree with your suggestion about nomenclature. (I only feared to
confuse people by using "cpo" in a new sense.)
3) I expected that you expected this result.
Regards
Kurt.
----------
PS to Albert:
This can be forwarded to types as well as my answer to Matthias if he
agrees.
------------------------------------------------------------------
Date: Mon, 31 Jul 89 17:22:02 CDT
From: Matthias Felleisen <matthias@rice.edu>
To: sieber@fb10vax.informatik.uni-saarland.dbp.de
Cc: meyer@theory.LCS.MIT.EDU, plotkin@src.dec.com, dorai@leto.rice.edu,
cork@leto.rice.edu
In-Reply-To: Kurt Sieber's message of 31 Jul 89 13:58 GMT-0100 <<8907311257.AA18435@fb10vax.sbsvax.uucp>>
Subject: full-abstraction for call-by-value
Kurt: here are some short answers.
> 1) Models:
>
> The relation between your model and my model is as follows:
> Your D^t is isomorphic (as a cpo) to my D^t_bottom
Your model is isomorphic to Gordon's partial function model (but it
also introduces a lot of extra notational inconvenience). Our model is
algebraically a little bit different because we have more bottoms.
> 2) Constant functions: ...
> ... a source of confusion is,
I only wanted to point out that
[bottom ==> bottom]
is a finite function in my model.
[But yes, I think it is confusing to think that (\x.5) denotes a
constant function: when applied to Omega, it diverges. Hence, it
doesn't denote the constant function and our model shows that.]
> 3) Short threshold functions:
>
> I can't see why this problem should disappear in your approach.
> Consider the (finite) function
> f = (0 => \x:i.bottom)
> of type (i -> i -> i), i.e. f n TERMINATES for n = 0 (with
> result \x:i.bottom) and diverges for n > 0. How can f be the lub
> of threshold functions of ``length'' 3 ?
The problem doesn't exist in my model: just use [0 ==> [bottom ==> bottom]].
I am sorry that I didn't realize that the problem doesn't even exist
in YOUR model because of the following:
for all d in D, [d ==> bottom] =~ {(x,bottom) | x in D}
and so you could have used [0 ==> [0 ==> bottom]] as the step-function
of length 3. [Note: In Gordon's model [d==>bottom] IS really the empty
function; one doesn't have to think of it as the empty function. In
our model, [bottom==>bottom] is a nice canonical name for it.]
> 4) Computational adequacy: ...
> Albert told me that Gordon has proved it before, but that he needed an
> ``unnatural'' operational semantics
That sounds right to me and confirms my intuition except that I
wouldn't call the semantics unnatural.
----------------------------
Albert: if you believe this correspondence to be of general interest,
please forward it to "types".