[Prev][Next][Index][Thread]
Plotkin on Meyer-Reicke paper on Continuations (218 lines)
Date: Thu 5 May 88 15:30:49-PDT
From: Gordon Plotkin <PLOTKIN@CSLI.Stanford.EDU>
....
In-Reply-To: <8805052057.AA00573@STORK.LCS.MIT.EDU>
Mail-System-Version: <SUN-MM(242)+TOPSLIB(128)@CSLI.Stanford.EDU>
Albert, I already got a preprint from Jon (MITCHELL---ARM). Herewith my
reactions: Albert, herewith a few thoughts on your paper with Jon
Riecke.First the paper makes me happy as it gives reasons why no
continuation- based semantics can be fully abstract , by which I mean that
any such semantics , C' should satisfy
C'[M]=C'[N] implies M=cN
, a much weaker thing than your conjecture and (no doubt) true
for the standard model of lambda-c.But your theorem 6 gives an
example of M, N with M=vN but not M=cN and hence not C'[M]=C'[N].
I wish I had known such examples when writing my paper.
(@article{Plotkin75,
Author={Plotkin, Gordon D.},
Title={Call-by-name, call-by-value and the lambda calculus},
Journal=tcs,
Volume=1, Year=1975,
pages={125--159}} ---ARM)
The results in your paper on lambda-v seem to be:
For any M,N
Lambda-v|-M=N implies Lambda-v|-M~=N~
implies M~=vN~
implies M=vN
but the first and third implications cannot be reversed.(I am
using M~ for the transform.)
One obvious conjecture , neither can the second implication be reversed.
These results are for a typed lambda calculus with arithmetic and
also the corresponding untyped calculus. I suppose/wonder about
the same results for the pure calculi where I am not so clear
about the congruences; they can be defined all right using
values (eg closed lambda terms) but I dont know if that agrees
with the above case , and especially doubt it for the typed case.
On the other hand what the equational calculus should
"really" be seems much more arbitrary with natural numbers and
recursion around; I suppose yours is the right "minimal" such
calculus though.
As you no doubt know, your proof that M1 =v M2 in Theorem 5 can be done
model-theoretically, they are equal in the evident( partial-function space)
model and the model is computationally adequate (what I prove in my
CSLI notes,or rather, claim there ) Another way that might interest you
is to proceed via lambda-p , the partial lambda calculus. One has that
M1=M2 is provable in lambda-p, and , just as for lambda-v, that M=c is
lambda-v provable iff M evaluates to c (of course one
proof of this latter fact is model-theoretic.....)(Oh yes, also P1=P2
is provable in lambda-p).
There should
be additional interest in lambda-p as it proves more equations and
hence might be of greater help with optimisation , and theoretically
typed lambda-v corresponds to partial cartesian closed categories,
an analogue of the total situation . The situation is not very simple, however,
there is an even stronger calculus mon-lambda-p the monotone partial
lambda calculus. All this and very much more in Moggi's thesis (to
appear!!)
Here are two more things:
(PLOTKIN INDICATES THESE ARE HIS CONJECTURES, NOT THEOREMS---ARM)
1. for all M,N lambda-v|- M~=N~
iff lambda-c|- M=N
iff lambda-c|- M~=N~
2 for all M,N M~=vN~ iff M=cN iff M~=cN~
One of these is a conjecture of yours. What do you think of the others?
And then there is lambda-p|-M~=N~ too of course.....
APPENDIX A brief intro to lambda-p ( typed and untyped considered together
here , pure calculus only)
Atomic formulae A are equations, M=N or existence assertions , E(M)
Sequents are G|-A where G is a set of existence assertions.
PROOF RULES G,E(M)|-E(M)
G|-M=M
G|-M=N
--------
G|-N=M
G|-L=M G|-M=N
--------------
G|-L=N
G|-L=M G|-N=K
---------------
G|-L(N)=M(K)
G|-M=N
------------ (x not free in G)
G|-\xM=\xN
G,E(M)|-M=N G,E(N)|-M=N (This is why the G's are needed)
----------------------------
G|-M=N
G|-E(x)
G|-E(\xM)
G|-E(N)
------------------
G|-(\xM[x])N=M[N]
G|-E(MN)
--------
G|-E(M)
G|-E(MN)
---------
G|-E(N)
(plus alpha-conversion)
Note the derived substitution rule:
G|-A H|-E(N)
--------------
G[N/x],H|-A[N/x]
Yours ever , Gordon.
-------------------------------------------------------------
Date: Fri, 6 May 88 10:57:46 EST
From: meyer
To: PLOTKIN@CSLI.Stanford.EDU
In-reply-to: Gordon Plotkin's message of Thu 5 May 88 15:30:49-PDT <578874649.0.PLOTKIN@CSLI.Stanford.EDU>
Subject: =v and =c
cc: riecke
Delighted with your fascinating comments. I'll be studying them closely with
Riecke after my current proposal-writing episode is over.
SOME QUICK REACTIONS:
I suppose/wonder about
the same results for the pure calculi where I am not so clear
about the congruences; they can be defined all right using
values (eg closed lambda terms) but I dont know if that agrees
with the above case , and especially doubt it for the typed case.
WE HAD THOUGHT ABOUT THIS. Our results don't need much more than some
terminating ``numeral-like'' combinators, say 3 and 4, a conditional test to
distinguish them, and a divergent combinator. The pure untyped calculus can
simulate this, so results seem to go through. PURE TYPED calculus seems too
weak, eg, can't use termination as an observable since everything does.
Adding ground constants but no conditional is still not enough as Church
numerals (lam f:int-->int.f) obs-cong (lam f:int-->int.(f o f)) wrt to
conditional-free contexts. So we chose to be ad hoc but sensible in choice
of typed calculus for now; think more deeply later.
As you no doubt know, your proof that M1 =v M2 in Theorem 5 can be done
model-theoretically, ... (what I prove in my
CSLI notes,or rather, claim there )
I PRESUMED IT MORE THAN KNEW IT, since we haven't yet found the study time your
handwritten notes require---and we have no copy of the CSLI notes. (I wish
you'd find a collaborator with expository ambitions to flesh out the notes
and put them in publishable form. There would be an appreciative audience,
including me and my students of course, and I can offer several publication
outlets.)
All this and very much more in Moggi's thesis (to
appear!!)
SEND COPY ASAP, please.
Here are two more things:
1. for all M,N lambda-v|- M~=N~
iff lambda-c|- M=N
iff lambda-c|- M~=N~
I ``KNEW'' THE FIRST `IFF' THOUGH NEVER ARTICULATED IT. NEVER THOUGHT OF THE
SECOND.
2 for all M,N M~=vN~ iff M=cN iff M~=cN~
One of these is a conjecture of yours. What do you think of the others?
And then there is lambda-p|-M~=N~ too of course.....
RIECKE AND I HAD DISCUSSED INCLUDING THE SECOND `IFF' AS PART OF THE CONJECTURE
IN OUR PAPER AS WELL, BUT HELD OFF FOR LACK OF TIME TO CHECK IT OUT. ARE
THESE CONJECTURES OF YOURS, OR HAVE YOU GOT THE RESULTS?
APPENDIX A brief intro to lambda-p ( typed and untyped considered together
here , pure calculus only)
CAN I FORWARD OUR CORRESPONDENCE TO THE TYPES LIST?
EXPECTING TO SEE YOU IN BOULDER.
REGARDS, A.