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-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx
Cc: meyer-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx, 
plotkin@xxxxxxxxxxx, dorai@xxxxxxxxxxxxxx
In-Reply-To: meyer-x+IGbNLxKNYFC4420IwThje48wsgrGvP@xxxxxxxxxxxxxxxx'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-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx>
To: matthias%rice.edu%eansb.uucp-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx
Cc: meyer%theory.lcs.mit.edu%eansb.uucp-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx,
        plotkin%src.dec.com%eansb.uucp-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx,
        dorai%titan.rice.edu%eansb.uucp-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx
In-Reply-To: <Matthias Felleisen's message of Sun, 30 Jul 89 13:49:59 +0200 
(MET dst) <<8907300520.AA07355-pl5bL5r1OTRNRPVWJXnxRw@xxxxxxxxxxxxxxxx>>.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-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx>
To: plotkin%src.dec.com%eansb.uucp-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx
Cc: meyer%theory.lcs.mit.edu%eansb.uucp-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx,
        matthias%rice.edu%eansb.uucp-DHPTTWqgmxzk1uMJSBkQmQ@xxxxxxxxxxxxxxxx
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-OhmvVRJSr/I@xxxxxxxxxxxxxxxx>
To: 
sieber-WOHuJR/SLnKM0MU9lROt9IUxn1rvdJyGZRV5cB5dno3gEf2P6hKOiQ@xxxxxxxxxxxxxxxx
Cc: meyer-Pk+Q08jrNjsK5/GGV6Q7qeW1CriLhL8O@xxxxxxxxxxxxxxxx, 
plotkin@xxxxxxxxxxx, dorai@xxxxxxxxxxxxx,
        cork-0/8oPpZgzcXV1CgomF1qdQ@xxxxxxxxxxxxxxxx
In-Reply-To: Kurt Sieber's message of 31 Jul 89 13:58 GMT-0100 
<<8907311257.AA18435-WOHuJR/SLnIiEUdjRziVSsGQWYsfwQaK@xxxxxxxxxxxxxxxx>>
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".