[Editor's note: This is the complete text of Bill Richter's second response to the "Bill Richter FAQ", in which he responds to Kevin Millikin's criticism of his first response. I have added a couple of editor's notes to explain Kevin's criticisms.] From: Bill Richter Subject: Re: Clinger's sloppiness in his RichterFAQ Newsgroups: comp.lang.scheme Date: 2004-08-21 17:55:12 PST kmillikin@acm.org (Kevin Millikin) responded to me in message news:<837a520f.0408210832.63f6ce74@posting.google.com> ... Let me first clarify my post, which I wrote in some haste & anger. By sloppiness, I'm only referring to Will's scholarship: what he said I did. There's a number of really interesting mathematical issues raised in Will's FAQ, And I don't mean to say there's anything sloppy about Will's thinking here. I think he's wrong, and I don't approve of the way he hasn't been willing to come to grips with these issues. I'm disappointed that we're not making more progress on what seems to me to be a very interesting interaction between pure Math (where sets 'n functions get whizzed around with ease) and CS/Logic (where the whizzing is actually seen to be justified by ZFC). But to me, an FAQ is a canon of distilled wisdom, and you'd get that impression from the way Will wrote in his links [Editor's note: ... ]. That sounds like real reflection took place, at a historical distance. I think it'd be fine if Will wrote instead [I immediately posted in response: ... ]. And it'd be even better if he'd stick a disclaimer on the FAQ page: "Here's some of the more ridiculous sounding things that Richter posted, and some of my wittier responses. But don't take this for a definitive account of the argument: Richter disputed all of my responses here on the group, and I'm not including everything. When I first saw the links listed , I thought, OK, Will's got a bunch of excerpts of his posts & mine, and he'll slant it to look like he "won", I can live with that. The error he had on the actual FAQ page bugged I refuted it here. But [Editor's note: ... ] sounds like he put a lot of thought into organizing the discussion after it took place. So I say Will's FAQ is lousy scholarship. I can't believe somebody would misunderstand me that wildly if they read my posts carefully, and thought about it afterward, and then organized it... Here's some really interesting math issues raised in Will's FAQ: 1) In what logical framework do we do DS, including Scott models? Constructivism, axiomatic ZFC proofs, the hurly-burly world of pure Math (where point set Topology resides), which is supposed to be formalizable by ZFC, but few pure Math folks know how. 2) What's the relationship between the compositionality of Nielson^2 and Tenant, where sem functions might possess denotational definitions, and C-F's compositionality, which is a property of the functions themselves? 3) What's the evidence that I made any dumb variable capture errors, either with the MIVT or Schmidt's Thm 3.13? Questions 2 & 3 are trivial to answer if we work in the pure Math world: Nielson^2 != C-F, and I made no variable capture errors. Maybe Will thinks we're working in a different logical framework, though. Back to haste and anger, I was discussing Will's FAQ with someone, who informed me that Will had clarified the question of the definition of compositionality. So I thought I had to look, and wrote him a long response, about that and the other Editor's notes, and I copied a third party, and I was massaging my introduction to address the 3nd party, and I was just blinded by rage, I couldn't see. So I thought, let's lower the violence level, how do we do this? So I thought: post it. Leave off the 2nd & 3rd party. At least I could see :) > 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. Kevin, I guess you're angry too, because that's clearly explained in Will's FAQ, which I quoted: [Editor's note: Bill completely misses Kevin's point, which was that Bill's "M[x <- V]" above is incorrect. According to Bill's definition of Phi, it should have been "E (M[x <- V])", which is not allowed in a definition of E by structural induction, which means that Bill's definition of E is not compositional.] Because his semantics is the totalization of the transitive closure of beta-value reduction: ((lambda (x) M) V) --> M[V/x] (where V is a value) How should you reduce it to a value? With E? Clearly not, even you have admitted that that's cheating and violates compositionality. Partly you're right, but this is too confusing, let's back up: My total (non-semantic) function E: LC_vExp ---> Value_bottom satisfies the Bill-compositionality equation E[(M N)] = Phi( E[M], E[N]) So if the V above wasn't a value, it would get "reduced" by E, and that's not cheating. That's what compositionality is supposed to do: E_1 of an phrase is some function of E_1 of the sub-phrases. The "cheating" issue is that my Phi is defined in terms of E: Phi = f_14: Value x Value ---> Value_bottom For U, V in Value, Phi(U, V) = E[ P[y <- V] ], if U = (lambda (y) P), bottom, otherwise Everyone knows you can't define E by structural induction on a Phi that's defined in terms of E! But I'm not doing that. Bill-compositionality just mean- that the E_i sem functions (E_1 is E + alpha-modding) and the f_ij functions (including Phi) satisfy some equations. So it doesn't matter what order the E_i & f_ij are defined in, at least from the point of view of bogus mutual recursion. [Editor's note: The first two sentences of the paragraph above assert that Bill did not define E by structural induction. That means Bill's definition of E is not compositional. The third sentence states that Bill's E_1 is just the composition of E with a quotient map. Therefore Bill's definition of E_1 is not compositional either.] But if, as you insist, extensional equality is all that matters, Yes, I do. Thanks. [Editor's note: Bill left out the conclusion of Kevin's sentence. Here is the complete text of Kevin's paragraph: Instead, you will use another function that just happens to be extensionally equal to E. But if, as you insist, extensional equality is all that matters, then didn't you in fact apply E to a term that is not a proper subterm of the argument? Since Bill grants the if part of that question, Bill did in fact apply E to a term that is not a proper subterm of the argument.]