[Editor's note: This is the complete text of Bill Richter's most definitive answer to the "Bill Richter FAQ". I have added editor's notes to explain why none of Bill's criticisms of the FAQ are valid.] From: Bill Richter Subject: Clinger's sloppiness in his RichterFAQ Newsgroups: comp.lang.scheme Date: 2004-08-20 20:59:23 PST I finally seriously read Will's "Bill Richter FAQ" . All the Math on the 1st page is nonsense, as I posted earlier, but I actually went through the links. To some extent, Will usefully explains that I learned a lot, and made a number of early errors. There's even some good information he didn't post. And the humor is pretty good, e.g. Q: What does Dr Richter think of this FAQ? It's hard to tell, because he changes his mind from day to day. That's true! But his FAQ is full of nonsense, which shows sloppiness on Will's part. I'll give almost complete responses to 2 links 4. Incorrect statements and/or specious reasoning. 6. Lunacy But first, let me re-refute the nonsense of the 1st page: Q: Why isn't his semantics 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) Substituting V for x yields a term that is not a subterm of the redex on the left side of that arrow. In a definition by structural induction, the meaning of the redex must be defined by a function of the meanings of its proper subterms. 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. [Editor's note: Bill quoted his own equation incorrectly. His last line above should be E(M[x <- V]), which applies E to a term that is not a subterm of the original argument to E. Therefore Bill's definition of E is not compositional, for precisely the reason stated in the Richter FAQ.] Q: Why does Dr Richter think his semantics is compositional? ... Since the identity function is compositional, Bill concludes that his operational semantics is compositional. False, and this is Will's usual sloppiness. I posted over & over that my OpS-ized semantics is compositional, because it satisfies the property of Bill-compositionality, and then I used Schmidt's Thm 3.13 to prove that Bill-compositionality = cls-compositionality, where cls-compositionality is defined to be C-F's definition with Will's 2 extra words added in: i.e. that the sem functions have a definition by structural induction. Using the different definition that Will seems to want to use below, I'd instead say that my sem function E_i have a denotational definition: the one given by my f_ij functions. What I proved by Schmidt's Thm 3.13 is that if you use the f_ij functions to produce sem functions BB_i by structural induction, then these functions BB_i are then equal to the functions E_i that I started with. Therefore, the E_i have a denotational definition. [Editor's note: Bill's notions of Bill-compositionality and of cls-compositionality do not coincide with the consensus definition of compositionality. As stated in the Richter FAQ, although often denied by Bill himself, most of Bill's E_i functions are identity functions, and Bill's definitions of those identity functions are compositional. Bill's E_1 is not an identity function, however. Bill's definition of E_1 is a slightly obfuscated composition of a small-step operational semantics (the E above) with an identity function, so Bill's definition of E_1 is not compositional.] [Editor's note: In the first excerpt for 18 July, Bill claimed to have proved that Bill-compositionality is equivalent to the "c.l.s. consensus definition of compositionality". Above, two days later, he dismisses the consensus definition as meaningless.] That's nonsense! What I said was meaningless is the idea that a function has a preferred definition. [Editor's note: Compositionality is a property of definitions, not of functions. Bill arbitrarily rejects this (23 June 2004), and arbitrarily insists that compositionality must be a property of functions. He then argues that our notion of compositionality is "meaningless" (20 July, 13 August) on the grounds that functions don't have preferred definitions. See below.] [Editor's note: Bill is the one who confused our notion of compositionality, which is a property of definitions, with his notion of compositionality as a property of the functions themselves. He says our notion is meaningless, and he also claims to have a proof that our allegedly meaningless notion is equivalent to his. See the excerpts for 23 June, 26 June, 1 July, 16 July (second excerpt), 18 July (first excerpt), 20 July, and 27 July.] No, that's extremely sloppy of Will. My confusion is that Will always said he accepted C-F's definition of compositionality, except that Will wanted to add 2 extra words DEFINED BY, inserted here: [The maps from syntactic domains to semantic domains] satisfy the law of compositionality: the interpretation of a phrase is DEFINED BY a function of the interpretation of the sub-phrases. Note that it's the maps which are compositional, and not some definition of the maps. So there's no way to equate C-F's definition with "our notion of compositionality, which is a property of definitions", unless one falsely believes that functions come with preferred definitions. This sloppiness of Will's borders on slander. I was extremely precise that what I said was meaningless was just this: that functions have preferred definitions. [Editor's note: Bill is denying that "is defined by" refers to a particular definition.] We define E[M] = V, if M |-->>_v V bottom, otherwise. [Editor's note: Richter is using the same letter E for two entirely different purposes. E is the existentially quantified unknown in his compositionality equations, That's just pure nonsense. I refuted this over & over. I defined E exactly as above! [Editor's note: See the FAQ's full category 4 excerpt of Bill's post for 8 July 2004.] and is also the totalization of the multi-step transition relation |-->>_v. Richter has also expunged the existential quantification of E from his exposition, so it is hard for a reader to tell which occurrences of E are which. This amounts to assuming the theorem he is trying to prove.] That's nonsense. I have a theorem Bill=cls-compositionality, and that means I don't have to define anything by structural induction. [Editor's note: Bill's theorem is irrelevant here. As can be seen below, Bill does not understand that the quantifier "there exists" binds the quantified variable or that the quantified variable has local scope.] [Editor's note: To prove uniqueness via Schmidt's Theorem 3.13, one must first prove that the EE_i satisfy the equations of that theorem. For Richter's perversely complex f_ij, this was not trivial.] That's an interesting admission. That's the reason why I'm not doing the identity semantics, even though Will often claimed I was. Will himself gave a proof of these equations for his 2nd ISWIM semantics, and I suspect Will's proof is cleaner than my oft-errata-ed proof. [Editor's note: In the category 4 excerpt for 4 July 2004, Bill claimed he was "100% done with a proof" that omitted an essential step.] [Editor's note: By definition, a context-free grammar has only a finite number of productions.] Schmidt doesn't use the phrase context-free grammar, or insist on a finite number of productions. [Editor's note: Bill doesn't recognize a context-free grammar when he sees one. Schmidt's notation implied a finite number of productions.] [Editor's note: Since "compositional" means defined by structural induction, Bill's last sentence above says Bill's definition of his semantic functions is not compositional.] This looks like an error! A function has lots of definitions, and one of them might be by structural induction. There's no preferred definition of a function. [Editor's note: Bill has rejected the fact that compositionality is a property of definitions, not of functions, so he cannot understand why his definition is not compositional.] [Editor's note: Apparently, Bill doesn't recognize that "Given functions f_ij...there exists a unique family of functions BB_i... such that..." is the technical way of saying the f_ij define the BB_i by structural induction.] That looks just like pure Math ignorance on Will's part. It doesn't mean that at. Something like this happens to be true, but it's a theorem, which I call Bill=cls-compositionality. This unique solution BB_i happens to have a definition by structural induction. [Editor's note: See what I mean?] [Editor's note: As I wrote in the passage that Bill quoted at the beginning of this excerpt, the fallacy is Bill's claim that the definitions of the f_ij can refer to the BB_i whose existence is asserted by the theorem. See also the first excerpt from 31 July, which gives a simpler example of the same fallacy.] It isn't a fallacy. It's just like the intermediate value theorem, which says, "given f, there exist e ...". You can actually apply this theorem to an f which is defined in terms of an e. f and e are just letters that refer to some sets in our ZFC-model. [Editor's note: Yes, it is just like the intermediate value theorem. See my response below to Bill's discussion of that theorem. Note that, in the paragraph above, Bill has backed off from his repeated claims (18 July, 22 July, 30 July, 31 July) that the definition of f can refer to the existentially quantified variable e. He now says only that f can be defined in terms of "an e", not necessarily the existentially quantified e. Unlike his earlier claims, this claim is true.] [Editor's note: ... By Goedel's Completeness Theorem, provability in first-order logic is equivalent to validity (truth in all models). Bill's "semantic proof in our model of ZFC" is hot air. ] I posted that myself (it's hot air) a few days later, to the guy who brought up Goedel's Completeness. That's a big thing I learned in this thread: I'm pretty busted in terms of understanding how pure Math is justified by ZFC. I'm really planning to figure this out, but none of my pure Math buddies know either. [Editor's note: There is no "ZFC-model theorem" that would justify Bill's mode of argument. As for his idea that the EE_i are bound variables for me but not him: We're talking about logic and mathematics here. The EE_i are bound variables. They have limited scope. Those are facts. Whether those facts are convenient for Bill is irrelevant.] That's complete nonsense. A statement "Given functions f_ij...there exists a unique family of functions EE_i... such that..." does not mean that the EE_i are bound variables. In pure Math proofs, any variables just refer to elements of our ZFC-model. It just says, given some elements in the ZFC-model (i.e. sets) that we're calling by the names f_ij, then there exist some other elements in the ZFC-model (i.e. other sets) that we're calling EE_i. This bound variables biz would only apply to a syntactic ZFC proof. That is, 1st order Logic proofs in in the language of set theory, using the ZFC axioms. I mean to learn how these proofs go. [Editor's note: Bill has very little understanding of logic or the structure of proofs. In particular, he does not understand that "there exists" binds the quantified variable, and gives it a local scope.] [Editor's note: All conclusions follow from a fallacious argument. The fact that some of those conclusions are true has no bearing on whether the argument is fallacious. Bill's definition of f in terms of e was carefully chosen to result in true conclusions, of course. despite his fallacious reasoning. And what is the fallacious reasoning? [Editor's note: Bill's fallacy is his claim that, when applying theorems of the form "for all functions f (with a certain property) there exists e (with a certain property)", the definition of f can refer to the existentially quantified variable e.] Almost any other definition of f in terms of e would lead to false conclusions, thereby exposing the fallacy. For example: Let e = 2/3. Define f in terms of e like this: f(x) = 3 * e * x - 1 Then, by Thm Mono-IVT, there exists a unique e in (0, 1) such that f(e) = 0. It is easy to check that f(1/2) = 0. Therefore 1/2 = 2/3.] What nonsense! f is *exactly* the function f(x) = 2x - 1, so f(0) = -1, and f(1) = 1. The e has been expunged from the discussion! f is just a name we're using for some set. Now Thm Mono-IVT says there's some unique e = 1/2 s.t. f(e) = 0, and of course that's true. There's no connection between the first e and the 2nd e. Will knew all this when he was taking Point Set Topology. [Editor's note: Bill correctly says there is no connection between the e that occurs within the definition of f and the e whose existence is asserted by the theorem. Therefore his repeated claims (18 July, 22 July, 30 July, 31 July) that the definition of f can refer to the e whose existence is asserted by the theorem must have been nonsense.] [Editor's note: The R5RS semantics has countable models, which include actual implementations. The R5RS semantics does not rely on any non-constructive mathematics.] Bah, everyone's always said that R5RS DS uses the Scott model approach of Stoy, which is the only reference cited here. There's nothing the least bit constructive about Scott models. I'm of course interested in learning about these countable models... [Editor's note: Bill Richter is hardly an authority on constructive mathematics. All of the Scott domains that are used in the R5RS can be defined constructively.] I don't believe we can compute the partial function curly-E[e]: U x S x K -> A in a finite amount of time. That would mean computing the actual domain of curly-E[e], and I bet that'd contradict the Halting problem. [Editor's note: curly-E[e] is the denotational semantics of the expression e. It is defined by a compositional, i.e. syntax-directed, translation of the expression into the meta-language of the semantics. Compilers routinely perform this translation or its equivalent in a finite amount of time.] As I keep saying, I doubt it. Maybe it's true. What is true of course is that compilers routinely calculate curly-E[e](r, k, s) in finite time, unless it's in an infinite loop. [Editor's note: Compilers do not calculate curly-E[e](r, k, s) at all. Bill does not understand the distinction between compile time and run time. Similarly, he does not recognize the distinction between the meaning of a phrase and the execution of a program that contains the phrase. This is a primary source of Bill's confusion.] [Editor's note: Halt is recursively enumerable. For other examples of computable partial functions and r.e. sets that Bill doesn't believe, see the excerpts for 22 June, 7 August, and 11 August.] That's something I learned, from MB, and I posted that I was wrong. I'm even getting an idea how to prove it: it's like the Goedel completeness theorem: we can write a program to print out all the consequences of the ZFC axioms. (BTW Goedel I says that's just not equal to the true theorems in a given model of ZFC.) In the informal proofs that pure mathematicians give, which Halmos tries to fit under the umbrella of Naive Set Theory, variables are just names for actual objects in our ZFC model.... [Editor's note: Naive set theory is inconsistent. Anything at all can be proved from naive set theory, and the proofs are very short.] Halmos explains this quite well, so maybe Will's not up on the book. But I'm glad I went this far, because I see Will's updating this. Now from Lunacy: BTW that's a good tip to look at Tarski's DS. Where can we read this? [Editor's note: Tarski's semantics of first order logic is presented in chapter 9 of Boolos and Jeffrey's undergraduate-level textbook, which Richter had begun to quote quite often.] Oh good, I asked Will that a # of times. And this is topical, because I'm in need of a better first order logic text. I don't like Enderton's book much, at least this edition, which he says is really Lighthouse's posthumous book. [Editor's note: All of Bill's arguments concerning what an engineer can't do or know apply equally to mathematicians, but Bill appears to believe that pure mathematicians transcend these limitations by working at some higher "semantic" plane of metaphysical reality. See the excerpt for 13 August, below.] But it's of course true that pure mathematicians can define sets that aren't computable. I was wrong about Halt not being computable, but it's not a computable subset of LC_vExp. The real line and Scott models can't be recursively enumerable, since they're not countable. [Editor's note: Halt is a recursively enumerable subset of LC_vExp. Bill's references to the "real line and Scott models" are irrelevant distractions.] No, no. It's largely the difference between syntax & semantics in Math Logic. Pure Math consists of statement, constructions, theorems & proofs that can probably be justified by axiomatic ZFC syntactic proofs. But pure Math isn't done that way at all. Pure Math that some ZFC model exists, and then does statements & proofs in this model. That's quite different from syntactic statements & proofs. [Editor's note: If proofs were done in some model of ZFC, as Bill here claims, they would not be valid proofs. A valid proof cannot depend on any one model. It must hold for all models.] I suppose, but it's irrelevant. In the pure Math world, we can't tell one ZFC model from another! None are known to exist! So it happens that all of our ZFC-model proofs are Will's valid proofs, so in particular, they have what I call syntactic ZFC proofs. Or at least that's what the set theory books claim. I'm behind the curve here. [Editor's note: This is lunacy. If there exist any models of ZFC at all, then we can construct (in Bill's sense of that word) a model in which the Continuum Hypothesis (CH) is true, and a model in which CH is false. By construction, we can tell the model that satisfies CH from the model that satisfies its negation. As for "ZFC-model proofs", that's just a phrase Bill invented so he could refer to garden variety informal proofs by a misleadingly technical-sounding name.]