This is a selection from messages that Dr Bill Richter has posted to comp.lang.scheme. ================================================================ 17 June 2004, replying to Lauri Alanko: > E[{f a}] e = let = E[f] e > in E[b] e'[i<-(E[a] e)] > ^^^^ > See the problem? Lauri, I don't quite follow you, but I do see a problem! Thanks! It's maybe impossible to show compositionality for my SICP-like E: Expressions -> (Env -> Values) because evaluating the 1st argument in {f a} changes the env/store. So let's unconflate Env & Store.... Was that your point, that I needed to unconflate to define E? [Editor's note: No. Lauri Alanko was explaining why a big-step operational semantics cannot be defined by structural induction. Alanko underlined the non-inductive part of the definition, but Bill doesn't see it.] ================================================================ 18 June 2004: > In Schmidt, p. 51, the existence of the meaning functions is proven > by structural induction. That's what "compositional" means: defined > with structural induction. I say that's false, Lauri. Can you give me an exact quote? ....So I assert that C-F & Schmidt do not make your definition, and furthermore, it's impossible to make a mathematical formulation of your definition of compositional. Can you check? ================================================================ 25 June 2004: I'm having trouble here, but largely I think I because I misstated my claim. I meant to say E was compositional in my sense. I don't know what "extensionally equivalent definition" or "well-founded" means, and I left out the base case of variables! Geez.... ================================================================ 1 July 2004: - Since standard reduction works by repeated application of value-preserving transformations, standard reduction is value-preserving. I'm not sure what that means. If E is already a value, then eval_s(E) = E. You don't do anything in that case. ================================================================ 21 July 2004: > > That's false, Joe, and I think that's the whole problem. > > What you wrote sounds like mutual recursion between E & Phi, > > which I am not doing. > > I'm sorry, I thought that when you wrote > > E[(M N)] = E[ P[y <- E[N]] ], if E[M] = (lambda (y) P), > > bottom, otherwise > that you meant [it]. > > I did mean it. But it's not a definition. It's a theorem, > probably due to Plotkin or F-F, but I gave a proof anyway, in my > 1st ISWIM post. Will reproved this result (in his context) in > his 2nd ISWIM post. Ok. It is *vitally* important (to me) that definitions and theorems be explicitly marked as such, otherwise I won't be able to make sense of anything or be able to contribute. Great, Joe. I certainly thought I was clear on this point.... ================================================================ 22 July 2004, quoting Clinger: Your consistently sloppy exposition, Bah.... and repeated refusals to clarify the important points (though you have gone on at great length about unimportant stuff), have made it impossible for us to tell whether your f_14 is well-defined. You just misunderstand what I'm doing. ================================================================ 23 July 2004, quoting Marshall: Does *this* model your semantics? I sure couldn't tell. I think we should take this discussion off-line. I want you to write an entire file of case-sensitive PrettyBig DrScheme code, put it on your web site, and *email* me when it changes, and I'll grab it it, and email you back with suggestions. Or else just email me the code. Nobody else here needs to see it. You can have huge files now, and we won't have to wait for the Google-Group 3--8 hour delay. I promise you I'll go through it with you. ================================================================ 26 July 2004: > Modding out by alpha-equivalence looms large in my mind because > F-F & Barendregt make a big deal out of it. Barendregt does not make a big deal out of it. Barendregt says we will quotient terms by alpha and identify terms accordingly. MFe and F-F also do not make a big deal out of it -- they say they will adopt the Barendregt convention, and move right along. So the big deal is in your mind, not in their writing (unless you can cite chapter and verse to the contrary). Furthermore, germane to the point Will was trying to make, your repeated discussion of alpha is distracting from the real technical issues. Shriram, we're mis-communicating. Both F-F & B quotient expressions by alpha. So I do the same. It's irrelevant to the technical issues. The real technical issue is Bill-compositionality. Please plug into this, to rescue the thread (& Will's time investment) from disaster. I'll big-picture it for you.... Will does not seem to understand either: my definition of Bill-compositionality; or my interpretation of Schmidt's Thm 3.13; or my proof of Bill = c.l.s.-compositionality.... IMO Will's problem in understanding my semantics is this: by not understanding my def of Bill-compositionality, he rewrote my posts, so as to define my semantic maps by structural induction. That easily leads him to nonsense, which he then attributes to me. When I try to explain to Will how he misread my posts, he brings up alpha. ....If Will would restrict himself to my 2nd ISWIM post, he would have no opportunity to task me about alpha. But he's really set on winning this argument with me. Cooler heads need to prevail. Now Will's right that if you impose structural induction on my 2 ISWIM posts, then it's nonsense.... ================================================================ 27 July 2004, quoting Blume: "Your" semantics (the one that does not need Scott models) is a joke, as Will said. Will did great work, but he showed no understanding of what I was doing, so when you quote Will, I have no idea what you mean.... Well, if you mean that one can define a function g in a compositional manner in terms of another function f which "happens" to have the same graph as g, then, yes, you can do that without using Scott models. Is that your point? If so, why are we wasting any time with this? I don't understand what this means. We're just having a Math discussion about compositionality. You & others 2 years ago claimed that I could not define compositional semantic functions in my OpS-ified way.... The biggest difference I note between your semantics and mine is that you defined your semantic functions by structural induction, and I did not, until my followup to you, and I don't like to work that way. ================================================================ 29 July 2004, quoting Clinger: The reason everyone had to guess at Bill's semantic function was that his exposition was spectacularly errorful, vague, and incomplete. That's completely false, Will. The problem we're having is that you've failed to understand my definition of Bill-compositionality. I don't think I've been the least bit errorful, vague, or incomplete about Bill-compositionality. You however haven't lately responded to detailed informative Math posts of mine. [....] IMO you're misunderstanding me in the same way that my pure Math guys misunderstand me, and it's not really anyone's fault. The scientific method I now think only compels excruciating scrutiny in very narrow cases, things you can check by an experiment, especially an experiment that you're publishing that you've completed. You're saying I'm wrong about things that you don't seem to have thought about very carefully. That's what my pure Math guys do. I'm trying to publish bug-fix papers about stuff that they claim is well known, even though they don't seem to understand it themselves. But that's not something you can do an experiment about: whether something is understood is a question about somebody's mental states. We can't do experiments about mental states :) ================================================================ 30 July 2004: But I don't think that you understand what I did at all. When you wrote that my semantics was compositional, I think you were really referring to Will's 1st ISWIM post. And if so, there's no reason for you to think about my Bill-compositionality definition yet. It has nothing to do with Will's 1st ISWIM post, which we all agree is a joke. But what only you & I understand is that it's compositional. That's the only reasonable place for you to plug in here. You don't seem to "get" the joke that your construction is (and that Will Clinger has been referring to for almost too long by now). You're making a serious error here, by believing that Will correctly described my work. He didn't. His joke semantics wasn't mine. ================================================================ 30 July 2004: I'm frustrated by folks authoritatively writing about my posts without citing them, and apparently even without even reading them. [Editor's note: As Blume replied, "We are all frustrated by folks authoritatively writing about things they evidently don't understand."] ================================================================