[Prev][Next][Index][Thread]
meyer to plotkin re full-abstraction for call-by-value
Date: Tue, 18 Jul 89 18:10:01 EST
To: plotkin@src.dec.com
In-reply-to: Gordon Plotkin's message of Fri, 7 Jul 89 10:01:23 PDT <8907071701.AA29042@jumbo.pa.dec.com>
cc: sieber%fb10vax.informatik.uni-saarland.dbp.de@relay.cs.net, bard,
riecke, trevor
Date: Wed, 28 Jun 89 14:21:30 EDT
From: bard@theory.LCS.MIT.EDU
To: GDP%ecsvax.edinburgh.ac.uk@nsfnet-relay.ac.uk
Cc: meyer@theory.LCS.MIT.EDU
Subject: Bottomless CPO's and partial functions
Kurt Sieber remarked that there was an obvious categorical equivalence
between your category of bottomless cpo's and partial functions, and the
category of ordinary cpo's and strict functions.
(PCPO -> CPO_strict:
B(D) = D + a bottom element B(f) = \x. f(x) if it's defined,
bottom otherwise
CPO_strict -> PCPO:
C(D) = D - {bottom} C(g) = \y. g(y) if it's not bottom, undefined
otherwise)
Since this is such a natural equivalence of categories, we were
wondering why you chose to use the somewhat less familiar bottomless
cpo's and partial functions. Are we confused about something?
Thanks, Bard Bloom scribe for Kurt Sieber and Albert Meyer
--------------------------------------------
Date: Fri, 7 Jul 89 10:01:23 PDT
From: plotkin@src.dec.com (Gordon Plotkin)
------- Forwarded Message
Return-Path: <plotkin>
Received: by jumbo.pa.dec.com (5.54.5/4.7.34)
id AA02483; Thu, 6 Jul 89 17:20:04 PDT
Date: Thu, 6 Jul 89 17:20:04 PDT
From: plotkin (Gordon Plotkin)
Message-Id: <8907070020.AA02483@jumbo.pa.dec.com>
To: ma (Martin Abadi), bard@edu.mit.lcs.theory, meyer@edu.mit.lcs.theory
Cc: plotkin
Subject: Re: bottomless cpo's
In-Reply-To: Your message of 29 Jun 1989 0931-PDT (Thursday).
<8906291631.AA08080@jumbo.pa.dec.com>
Well here is some kind of reply.
1. If you are working intuitionistically they are not equivalent. You
might care about this if you are working in some topos to find a model
of some programming language.
2. A propaganda point: I wanted to say that bottom gets in the way for
many reasons, so it would be very odd to have it, by using cpos with
bottom and then effectively taking it out via strict functions. As you
say the one with strict funstions is familiar, but that is because we
are familiarly used to having bottom and that is what I want to reject.
3. Somehow I find that when thinking of the category of strict
functions then I think of it as a closd category. But when I think of
the category of partial functions I think of it as a category of
partially Cartesion Closed category and hence a model for the partial
typed lambda calculus which is what I want.
-----------------------------
Your comments confirm our understanding.
Kurt Sieber believes he has worked out full abstraction for the
call-by-value version of PCF with parallel-OR and your ``standard''
partial cpo's starting with discrete base types and taking patial
continuous functions as morphisms. I got the impression that Kurt thought
it came out fairly straightforwardly, which surprised me, since from prior
conversation with you, and a recent conversation with Moggi, I though full
abstraction in this case was open. In any case, the result should be put
into the literature, don't you agree?
It seems to me that points 2 and 3, with which I agree, also highlight a
slightly frustrating point about call-by-value: a crucial part of the
computational scenario involves the behavior of meaningless terms--which
may appear in interesting ways as subterms of meaningful terms. Partial
function semantics, by definition, doesn't explain anything about this
behavior of meaningless terms. So syntax starts to take on an important
role independent of semantics. This seems to contrast with the situation
when using total functions and standard CCC's, where the whole story is
pretty well captured semantically.
For example, in the call-by-value case, knowing the meaning of CONDitional
doesn't tell one that it evaluates as a ``special form'' with the property
that (COND true 1 meaningless) evaluates to 1--the semantics can't explain
how a term denoting a partial function behaves when it is syntactically
``applied'' to meaningless things. Samson Abramsky suggested to me that I
shouldn't think about COND, but only about categorical sums (co-products)
where the sum functor serves the role of COND. I'm still not clear enough
abou the story to figure out whether Samson's remark offers the resolution
of my concern--are there any other bits of syntax I might have expected to
have available, like COND, which I have to give up in order for partial
function semantics to determine the behavior of all well formed terms?
Also, can we forward this correspondence to TYPES?
Regards, A.
---------------------------------------------
-------------------------------------------
-------------------------------------------
Date: 24 Jul 89 15:42 GMT-0100
From: Kurt Sieber <sieber%fb10vax.informatik.uni-saarland.dbp.de@relay.cs.net>
To: meyer%theory.lcs.mit.edu%eansb.uucp@relay.cs.net
In-Reply-To: <meyer@theory.lcs.mit.edu's message of Tue, 18 Jul 89 21:31:08 +0200 (MET dst) <<8907181157.AA00588@stork.LCS.MIT.EDU>>.de>
Subject: FA
Date: Mon, 24 Jul 89 16:41:45 +0200 (MET dst)
Here is a summary of my full abstraction result for a call-by-value
version of PCF:
Abstract:
=========
Following an idea of Plotkin we use "bottomless cpos" and "partial
continuous functions" for defining a denotational semantics of
call-by-value PCF. Full abstraction is proved in this purely
denotational setting (i.e. without referring to some operational
semantics).
Conventions:
============
"bcpo" means "bottomless cpo", i.e. a partial order which is closed
under limits of nonempty directed sets, but which does not necessarily
have a least element.
Let D,E be bcpo's.
Then the lifted bcpo D_bottom (which is of course a cpo) and the bcpo
[D -> E] of continuous functions are defined as usual (note that
continuity does not refer to bottom, so there is no problem with the
definition).
Semantics of types:
===================
For each type t we define a bcpo D^t as follows:
- D^unit = {()} (a singleton)
(the ground type unit is added only for convenience)
- D^int = {0,1,...} ordered by "=",
- D^bool = {tt,ff} ordered by "=",
- D^(s->t) = [D^s -> D^t_bottom] .
It is my understanding that the latter is (just another notation
for) Plotkin's "partial continuous functions from D^s to D^t".
The general setting for denotational semantics:
===============================================
Constants of type t are interpreted in D^t.
Variables of type t are mapped to D^t via a value assignment e.
BUT: For every lambda-term M of type t and every value assignment e
the meaning [[M]]e is defined as an element of D^t_bottom (!!!).
In Moggi's terminology (cf. his LICS 89 paper):
- D^t contains the VALUES of type t
(values are assigned to constants and variables),
- D^t_bottom contains the COMPUTATIONS of type t
(computations are the meanings of terms).
Constants and their interpretations:
====================================
(): unit
0,1,...: int
tt,ff: bool are interpreted as usual
succ, pred: int -> int
zero?: int -> bool
Parallel conditional:
---------------------
pcond has arguments of function type, in order to avoid evaluation of
the wrong branch:
For every (ground) type t let
pcond_t: (unit -> bool) -> (unit -> t) -> (unit -> t) -> t
pcond_t b f g = f() if b() = tt
g() if b() = ff
glb(f(),g()) if b() = bottom.
"if M then N else P" can then be considered as an abbreviation for
pcond (\x: unit. M) (\x: unit. N) (\x: unit. P)
i.e. lambda abstraction is used to delay evaluation of M, N, P.
Y-operators:
------------
They are only defined for function types:
Y_(s->t): ((s->t) -> (s->t)) -> (s->t)
Y_(s->t) f = least fixed point of f': D^(s->t) -> D^(s->t),
where f'gd = bottom if fg = bottom
fgd otherwise
Note that:
- D^(s->t) is always a cpo: its least element is the "empty partial
function" \x:s.bottom ,
- but f: D^(s->t) -> D^(s->t)_bottom,
hence f must first be "transformed" into f'.
Inductive definition of the semantics:
======================================
- [[c]]e = interpretation of c
- [[x]]e = e(x)
- [[MN]]e = bottom if [[M]]e = bottom or [[N]]e = bottom,
[[M]]e ([[N]]e) otherwise
- [[\x.M]]ed = [[M]](e[d/x]) for every d in D^t
Full abstraction:
=================
Equality between lambda-terms is defined as usual:
M = N iff [[M]]e = [[N]]e for every value assignment e
Observational congruence is defined "denotationally":
M obs_cong N iff [[ C[M] ]] = [[ C[N] ]]
for every closed ground type context C[.]
Theorem (full abstraction):
---------------------------
M = N iff M obs_cong N
Sketch of the proof:
--------------------
Nearly everything works out as in Plotkin's proof for call-by-name
([Plotkin77]):
(a) each element is the lub of a directed set of finite elements;
(b) the finite elements of type (s->t) are exactly
(i) the empty function \x:s.bottom and
(ii) all (existing) lubs of finitely many threshold functions (d=>e),
where d,e are finite;
(c) each finite element is definable by a closed PCF-term.
It follows that each element is the lub of a directed set of definable
elements, and then full abstraction follows as usual from continuity.
Two technical differences to the call-by-name situation are worth
mentioning:
- a constant function \x:s.d (d in D^t) is NOT finite,
- 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.
I assumed that these threshold functions of different length might
cause (at least notational) problems in adapting Plotkin's proof of
(c). Hence I used the form (s->t) (instead of (s1->...->sn->t)) in
my induction over types, and then I had to change the induction
hypothesis to:
Each function f: s->t which is the lub of finitely many threshold
functions of the form (d=>e) AND A CONSTANT FUNCTION, is definable.
Reference:
----------
@article{Plotkin77,
author = {Gordon D. Plotkin},
title = {{LCF} Considered as a Programming Language},
journal = tcs,
volume = 5,
year = 1977,
pages = {223--256}}
----------------------------------------------------------
---------------------------------------------------------
-------------------------------------------------------------
Date: Fri, 28 Jul 89 11:38:28 PDT
From: plotkin@src.dec.com (Gordon Plotkin)
To: meyer@theory.LCS.MIT.EDU
Cc: plotkin@src.dec.com
Subject: Re: [sieber%fb10vax.informatik.uni-saarland.dbp.de@relay.cs.net: FA]
In-Reply-To: Your message of Thu, 27 Jul 89 18:20:14 EDT.
<8907272220.AA00250@stork.LCS.MIT.EDU>
Albert and Kurt, first your (Kurt's) work certainly looks right to
me. I cannot resist the propaganda comment that it again shows, at least
to me, that working with bottom explicitly is clumsy. Did you try
it with partial functions instead?
One gripe I do have is nomenclature. I
don't like naming things by what they do not have , e.g. , bottomless cpos
, bcpos. I think Reynolds' predomains is better or even precpos, but not
much. I would propose using cpo for a generic notion, specified precisely
in any context. For precise terminology, why not have modifiers for the
"c"? Thus I propose an extra "p" for pointed when there is a bottom (I am
supposing we do not want to use pointed partial orders in which the point
is not the least element). And lets use an "w" (omega) for having lubs of
increasing w chains, and use a d for lubs of directed sets (following
Johnstone's(?) directed complete partial orders) or , equivalently , an
"i" for inductive. So what you call a bcpo I would call a dcpo or an icpo.
What people usually work with are the dcppo's or the w-cppo's. What do you
think?
Turning now to the older e-mail from Albert, first on Kurt's work the
question was open. This was not because I (don't know re Eugenio) thought
it difficult but rather because I expected it to be straightforward but
had not tried it. Kurt's experience confirms this. I agree the result
should be in the literature. (It is certainly good to know that it really
does work out OK).
On the next two paras, I am in pretty well total disagreement. Partial
function semantics does explain something about about the computational
behaviour of meaningless terms. What it says is that they do not have any
behaviour! Less jokingly, a term M has no meaning iff its evaluation does
not terminate. If you put in bottoms everywhere a la Kurt, then this
becomes: M denotes bottom iff it does not terminate (closed M of ANY type).
For me this is just like the story with total functions and standard ccc's
except here the story works out even better in my eyes (cf the work of
Cosmodakis for the total total story). By the way, in contrast to the full
abstraction result above,I have established the above correspondence for
a rather rich typed lambda calculus.
Turning to the case of COND, I believe, in opposition to Samson that one
should think about it, and there is a simple connection with coproducts.
But one should not take the meaning as a partial function (e.g.) from
bool*N*N to N. Then your difficulties do arise. Rather, much as Kurt does
with his pcond, take it as having type bool*(unit->bool)^2 -> bool.
(I am thinking of the partial arrow here, but of course you can do it with
bottoms if you want.) Then interpret (COND true 1 meaningless)
as COND(true,lambda x.true,lambda x.meaningless) if you see what I mean.
The relation with coproducts is that bool is unit + unit in the category of
dcpos and partial continuous functions, so one can take COND to be
lambda t,m,n. [m,n](t), using the partial lambda calculus and the [ , ]
construct for coproducts. In the language mentioned above, there was no
explicit COND but the types were closed under coproduct. I do not think
ther are any bits of syntax you have to give up at all!
Do forward this correspondence to TYPES.
All the best,Gordon.