[Editor's note: This is the complete text of Bill Richter's second response to Kevin Millikin. I have added one editor's note, not counting this one.] From: Bill Richter (richter@math.northwestern.edu) Subject: Re: Clinger's sloppiness in his RichterFAQ Newsgroups: comp.lang.scheme Date: 2004-08-22 19:01:36 PST kmillikin@acm.org (Kevin Millikin) responded to me in message news:<837a520f.0408210832.63f6ce74@posting.google.com>... Sorry, Kevin, I blew my response, as Will explains on his RichterFAQ. But first, let me explain that Will may well be right in one of our long-standing argument: My connection is bad now, so I won't cite Will, but essentially Will claims that I don't understand how lexical scope, bound variables, quantifiers work in math proofs. Will may well be right! It's irrelevant to the compositionality debate, but it may well show yet another aspect of the pure Math world that I don't know how to rigorize. Let me explain: In all my years in the pure Math world, I never once heard about lexical scope, or was ever told how one decides which set a variable f refers to, if there are several f's floating around. We pure Math folks learn to do this instinctively, and we never make mistakes, to my knowledge, which in practice (such as this comp debate) is all we care about, but there's an interesting theoretical point: I don't know what the rules are! It's possible that it's just as Will says, and I hope we can get back to this. More details: I first heard of lexical scope from K&R's C book, and it seemed very mystifying. Then later in Emacs & Scheme, I heard about dynamic vs lexical scope, but I still didn't understand. I remember saying to myself: "Lexical scope means you just look at the source code. But what do you look at?" Then finally, from F-F's LC_v notes, I saw that in a lambda exp (lambda (x) M), that the scope of x is M. Duh!!! Everyone here know this quite well, of course. So this x binds every free occurence of x in M, which are now called bound variables in (lambda (x) M). And I was really happy to figure this out! This didn't "click" with anything I'd ever heard in the pure Math biz! Now maybe it's easy to forget with Will's continual abuse of my math skills, but going by # of MathSciNet papers, I come in 2nd (7) to MFe (11), and Will's in 3rd (4, I think, which is a lot for a CS guy: I'm sure Will has 100 pubs, but this is just Math Reviews). And I'm finally grokking lexical scope 3 or 4 years ago! And just recently, Will continued my education, by explaining that in 1st order Logic, the quantifiers \forall and \exist work just like lambda w.r.t lexical scope and bound vbls. What a revelation! Now I'm quite ready to cede the point to Will yet, because there are serious differences between 1st order logic proofs and what we call proofs in the pure Math biz. But heck, he may well be right, even though it plays no role on the comp debate. It's on my to-do list! Another point: Stephen Bevan asked me an interesting question: essentially if I could play my compositionality games with Neilson's language While. And I whinged, it's too hard, but (Stephen, I can't email today) it's easy, and it's a good exercise. I can define easily Bill-compositional sem functions, using a one-step reduction function R and induction and the ZFC subset axiom. As Stephen told me, the only difficulty is the while statement. Thanks, Stephen! > > That's nonsense. My sem functions satisfy Bill-compositionality > > because of the equation > > > > E[ ((lambda (x) M) V) ] = Phi( E[ (lambda (x) M) ], E[ V ] ) > > > > = Phi( (lambda (x) M), V ) > > > > = M[x <- V] > > > > the last by my definition of Phi. It's really sloppy reasoning for > > Will not to understand this, because I posted it over & over. > > No, it's sloppy reasoning for you to claim it. I sure hope the result > is not M[x <- V], but that you reduce *that* expression to a value. Sorry, Kevin, I blew my response. As Will explains on his RichterFAQ, you're objecting to my typo which he spotted & I fixed: it should be E[ M[x <- V] ], not M[x <- V]. > How should you reduce it to a value? With E? Yes, as I've posted over & over. > Clearly not, even you have admitted that that's cheating and > violates compositionality. No, it's fine, as I've explained over & over, most recently in this thread, except for this unfortunate typo you & Will alertly spotted. Sketch: I first prove my sem functions are Bill-compositional, which only requires that some equations be satisfied, mainly the one here E[ ((lambda (x) M) V) ] = Phi( E[ (lambda (x) M) ], E[ V ] ) Then by the proof of Schmidt's Thm 3.13, my sem functions E_i have a denotational definition. There's no opportunity for your "cheating" in this step: I just apply Thm 3.13 to the f_ij function I defined in the Bill-compositional phase, and, voila! Thm 3.13 gives me some functions that happen to be equal to my original E_i. [Editor's note: Bill's semantic functions are Bill-compositional, which is a notion Bill invented. Bill is counting on his readers to forget that Bill-compositionality does not imply compositionality. Bill's definition of his semantic functions is not compositional.] > then didn't you in fact apply E to a term that is > not a proper subterm of the argument? I did, but so what? Will claims this objection is decisive on his 1st page of his RichterFAQ, but I refuted that in this thread. Sketch: Bill-comp only means that certain equations hold, esp the equation just above. That's it. So if Phi is defined in terms of E, it matters not a whit. Now if instead, we were setting up a structural induction, it would matter a lot. Hey I didn't know this before, so let me drag it out: If we tried to do a structural induction with equations like E[ ((lambda (x) M) N) ] = E[ M[x <- E[N]] ], everyone would say that's ridiculous. How's the induction gonna work? We're not simplifying things necessarily. The RHS must be some already-defined function applied to x, M & E[N]. BTW I'll recall that E is not my sem function anyway, but it's close: E_1 is E composed with the function that mods out by alpha equivalence. But the E_1 equations quickly move to E equations, because all the action takes place in F-F's LC_v.