[Prev][Next][Index][Thread]
reasoning about continuations (195 lines)
Date: Wed, 6 Apr 88 15:38:44 CDT
From: Matthias Felleisen <matthias@rice.edu>
To: meyer@theory.lcs.mit.edu
In-Reply-To: Albert R. Meyer's message of Thu, 24 Mar 88 11:48:17 est <8803241648.AA04444@STORK.LCS.MIT.EDU>
Subject: hello
I have finally received the preprint of your invited LiCS talk.
Despite your less than kind words for my work:
``... (and don't call my attention to [5,4], which, despite
a titular claim, don't fill the bill.)''
I have enjoyed reading it. The paper clarifies another time some
fundamental differences between us ``symbol pushers'' and
semanticists.
I guess that enough people have pointed out the typo on top of page 4,
right column.
In your references, I miss an important paper on semantic principles,
my personal favorite,
Plotkin, Call-by-name, call-by-value, and the \-calculus. TCS 1.
1975(4?).
[This paper contains the most important guideline for my own current
research programs: languages come first, logics and models come
afterwards (my paraphrasing). This is quite a contrast to your attempt
to find an interpreter (an operational semantics, i.e. a language) so
that Scott domains are completely adequate. But let's not be picky on
that. This is only philosophy. ]
More importantly, Plotkin's paper addresses the issue of normal-forms
versus values in this paper (see your own discussion on page 6). The
point is that nobody who really computes is interested in
normal-forms. Everybody cares about values, however, including people
w/ lazy functional languages.
% ----------------------------------------------------------
But now to our own work. I guess we used key words that got you
upset/excited in your role as semanticist. I believe it is the word
``reasoning.'' We use this word to mean ``proving (informally).''
Thinking about programs. I know that semantics offers me a nice way of
thinking about programs. But that doesn't mean we should throw out the
baby w/ the bath water. Why not use the beta-reductions to perform some
simple correctness arguments? Why not use symbolic reductions as a
help to understand the effect of programs?
I believe beta-reductions are interesting and the work that you
reference was a first attempt to find similar rules for programs that
require imperative(!) control operations. The requirement is, of
course, that such rules be conservative wrt to beta or beta-value
(whatever you start with: I prefer the latter). That's what I meant in
San Diego when I said that I have conservative rules. It was clear to
me, and should be to everybody working w/ continuations, that the
extension of operational equivalence is {\it not\/} conservative.
After all, control operations introduce effects, operational
equivalence measures effects, and hence it would be terrible if this
didn't show up. Because of this I find calculi more interesting: I can
freely move around between the various fragments and my equations
always hold! BUT I AM AWARE that calculi (algebras in Scott's words)
are insufficient for more complex arguments. My current escape is to
use equations in operational equivalences and label them as
potentially unsafe. Then, when I go to a richer language, I only need
to check these labeled proof steps. (I am pragmatic ...). I believe
that in these respects we have filled the bill, even though
we may have used the wrong words.
[A picture may help: = stands for my (syntactic) calculi on
continuations and state, =~ for operational equivalence, v for
call-by-value, c for control, s for state manipulation (assignment):
==> =_c
=_v { } ==> =_{c,s}
==> =_s
| | |
| | |
v v v
=/=> =~_c
=~_v { } =/=> =~_{c,s}.
=/=> =~_s
The arrows mean equality1 implies equality2, a / means not!]
I am surprised at your negative attitude towards continuations. I find
(imperative) assignments much worse. Just like you find expressions
that are operationally equivalent (=~) in a functional programming
language fragment but differ in control languages, you find the same
thing occurs when going from functional to state manipulating
languages, e.g.,
(\fg. (let (x (f 0)) (g x x))) =~ (\fg.(g (f 0) (f 0)))
in \Lambda, but not in \Lambda + :=,
use C[ ] == (let (c 0) ([ ](\x. (begin c := c+1; x)) (\xy.c)))
(call-by-value) for a context that distibguishes the two expressions.
Is this by accident or an oversight? I presume you don't like
assignments either. Just thought I should mention that.
[But then a natural questions comes up: do we (semanticists in all
camps) understand stores and store-passing style (a la denotational
programming) and their connection to direct semantics? Is there a
trivial answer that I am overlooking or has anybody written something
on that?]
Sorry, for writing that much. Perhaps it helps to provide some better
understanding for my ``titular claims.''
Regards -- Matthias
-----------------
Date: Thu, 7 Apr 88 11:34:15 EST
From: meyer
To: matthias@rice.edu
In-reply-to: Matthias Felleisen's message of Wed, 6 Apr 88 15:38:44 CDT <8804062038.AA07871@leto.rice.edu>
Subject: hello
Delighted to hear from you and looking forward to responding in detail. All
I have time for now are two comments:
(1) I like your work and need it to build on. My criticism is just of the
titular claim in your earlier paper that the confluent conversion theory you
set up enables one to ``reason'' about continuations. Well of course it
DOES---conversion in confluent systems can be an effective way to learn about
lots of code, and your contribution of a clean model of a call-cc interpreter
based on reduction is very valuable. But in the end, as I think you may
agree, reduction/conversion amounts to SYMBOLIC EXECUTION, and there are any
number of important and even ``obvious'' equations which can't be proved in
this limited way. I think a paper on reasoning like yours should point out
the limitations as well as the strengths of the reasoning methods developed.
I hope you'll forgive me for the provocative comment in my paper, but it was
made in the spirit of appreciative criticism, and I hope will serve us all
well if it calls attention to these interesting issues.
(2) I am not negative about continuations, just anxious. I don't claim there
is no effective general methodology for reasoning about observational
congruence of call-cc expressions, just that one is NEEDED, and until it
appears, their value (to me at least) as a simplifying notion remains
unclear. Remember the title of my paper with Reicke is that ``Continuations
MAY be unreasonable'', NOT that they ARE unreasonable. I just don't know
yet.
MAY I FORWARD YOUR NOTE AND THIS REPLY TO MY TYPES AND LOGIC EMAIL LISTS?
Regards, A.
-------------------
Date: Thu, 7 Apr 88 11:55:41 CDT
From: Matthias Felleisen <matthias@rice.edu>
To: meyer@theory.lcs.mit.edu
In-Reply-To: Albert R. Meyer's message of Thu, 7 Apr 88 11:34:19 est <8804071634.AA11016@STORK.LCS.MIT.EDU>
Subject: hello
True: we actually agree on most points.
(1) Control (continuation) operations are more difficult to understand
than functional operations: YES! But I
(2) I know that reduction/conversion theories are not the ultimate
means to ``reason'' about all ``controlled'' programs. Indeed, Carolyn
Talcott has built in my symbolic rules into a proof system for
operational equivalences. Her student, Ian Mason, has tried something
similar for first-order destructive Lisp; recently, they have extended
this to h.o. destructive Lisp. I will send you their mostly
unpublished manuscripts. I have tried point out in my previous msg why
I think calculi are interesting and important in conjunction w/ this
work.
(3) I would also love to see a good denotational approach of working
with ``controlled'' programs. That and the previous point is what I
meant in the conclusion of my TCS paper.
(4) I believed that the problems of a calculi-approach were obvious
and didn't require extra hints. I have tried to fix that in my Lisp
and Functional Programming paper and will send you a draft of that
one, too.
With regard to forwarding. I have not had good experiences with
network discussions (rrrs-scheme, in particular), but I could try
again. You may want to edit out some of the irrelevant remarks (such
as this one: Raymond Smullyan's lectures show up again :-) .... )
Regards -- Matthias
P.S. A while ago you mentioned that you would add me to your
Logic&Types list. I take it that this hasn't happened yet?
-------------------
INSERT BY ARM:
I MUCH PREFER NOT TO EDIT, SINCE THE SPONTANEITY OF EMAIL---AMONG THE KIND OF
EXPERIENCED PROFESSIONALS ON THIS LIST ANYWAY---IS ONE OF ITS CHARMS.