From: Bill Richter Subject: Re: Clinger's sloppiness in his RichterFAQ Newsgroups: comp.lang.scheme Date: 2004-08-21 20:47:48 PST cesuraSPAM@verizon.net (William D Clinger) wrote in message news: ... > I have added Dr Bill Richter's message to the Bill Richter FAQ at > http://www.ccs.neu.edu/home/will/Ephemera/richterFAQ.html I'll respond to your juiciest new Editor's notes here, Will, snipping insults. First one from your original FAQ: [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.] Thanks, that's a great recommendation! I've gotten thru 2.5 pages already, and it is a biiiig improvement over Lighthouse. However, B-J do not seem to attribute this to Tarski, whose first index citation comes up in Ch 14, Q Representability (which I used to know!). [Editor's note: Bill quoted his own equation incorrectly. His last line above should be E(M[x <- V]), Correct, thanks. It should be E[ ((lambda (x) M) V) ] = Phi( E[ (lambda (x) M) ], E[ V ] ) = Phi( (lambda (x) M), V ) = E[ M[x <- V] ] the last by my definition of Phi. which applies E to a term that is not a subterm of the original argument to E. But that's OK! The Bill-compositional equation amount to E[ ((lambda (x) M) V) ] = Phi( E[ (lambda (x) M) ], E[ V ] ) and that's true. The only requirement for Bill-compositionality is that these equations hold between the E_i & f_ij E_i( Option_ij ) = f_ij ( E_ij1(S_ij1),..., E_ijk(S_ij{k_ij}) ) Therefore Bill's definition of E is not compositional It doesn't make sense even. E isn't a semantic function, but only E_1, which is the composite (as I've posted over & over) LC_vExp -mod-out-by-alpha-->> LC_vExp -E--> Value_bottom It's only the E_i (including E_1) that can be compositional. The proof that the sem functions E_i are Bill-compositional reduces to the equation above with E. 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. You seem to have just ignored what you cited directly above. As I just proved, "Therefore, the E_i have a denotational definition." Therefore, the E_i have a cls-compositional definition. As stated in the Richter FAQ, although often denied by Bill himself, most of Bill's E_i functions are identity functions, I denied it exactly once, and you flagged me right away, and I immediately admitted it was so. and Bill's definitions of those identity functions are compositional. Bill's E_1 is not an identity function, however. Great. That's all that I always claim. E_1 != 1. Glad that's done. 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.] What is that supposed to mean??? Every function F is the composition of F with the identity function. Let's do it: F = F \circ 1 What does `slightly obfuscated composition' mean? And what's the point? It's of course true that E_1 is "practically" equal to E. But that makes no difference. Once you see my E_i are Bill-compositional, then we argue about whether Bill-compositional sem functions have cls-compositional definitions. There's no reason to keep talking about my E & Phi at this point, unless you wish to finally respond to my post in MB's ML thread, where I proved from scratch that my E_i are defined constructed by structural induction via my f_ij. [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.] You keep saying this, and I keep saying that 1) the only meaningless thing is that functions don't have preferred definitions, 2) You only need to admit that C-F's definition is different. You sort of addressed this here below: Will always said he accepted C-F's definition of compositionality, except that Will wanted to add 2 extra words DEFINED BY: [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. [Editor's note: Bill is denying that "is defined by" refers to a particular definition.] I do sometimes, yes. I say that if a theorem states "the E_i are defined by structural induction" then it means the E_i have *some* definition by str ind. But what's the point? You can't possibly equate C-F-compositionality of maps (which is one thing) and cls-compositionality of definitions (which is something else). By C-F-compositionality, I mean including your words DEFINED BY. The obvious truth is that the sem functions E_i are C-F-compositional iff the sem functions E_i have a denotational definition iff the sem functions E_i are cls-compositional. Do you agree, Will? If so, we can stop arguing about C-F and what's meaningless. [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.] That's circular. The Editor's note for my 8 July post is the one I'm responded to right here, and it gives no evidence for this crazy claim of yours, that E is an unknown in my compositionality equations. [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.] That's easy to believe! Sure there weren't 2 essential steps missing? [Editor's note: Bill doesn't recognize a context-free grammar when he sees one. Sure, because Schmidt didn't define it. Schmidt's notation implied a finite number of productions.] I don't believe that, and you never claimed it when we were discussing it on cls. And the point is moot, since I switched over to your finite productions biz, it was much cleaner. Thanks again! [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.] Ah, it looks like you're right here, Will. I'll agree if I can insert one word to your original text: "Bill's [original] definition of his semantic functions is not compositional." But it's clear: my E_i have a non-cls-compositional definition, the original one, but they also a cls-compositional definition. You don't seem understand that yet, but you may, you may.... [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.] Bah, everyone who's ever passed a point set Topology course knows you can apply the MIVT (which says "Given f ... there exist a unique e ..." in a case when f is defined in terms of e. You have to careful, that's all. But yeah, my response left something to be desired. I should've just said we can of course apply MIVT to your example as well, where the 2 e's are different. I didn't need to respond to your insult that I'd blow that case, when e = 2/3 & then 1/2. 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: In particular, he does not understand that "there exists" binds the quantified variable, and gives it a local scope.] What I said above it absolutely true, and if you don't understand, then you don't know how the pure Math world works. I'll simplify it: IVT: "Given f ... there exist e ... such that f(e) = 0" means exactly that given some element in the ZFC-model (i.e. a set) that we're calling by the name f, then there exist some other elements in the ZFC-model (i.e. some other set) that we'll calling e, and then f(e) = 0. That is, if you plug in the actual sets named by f & e, you get 0 (also a set). This is the important point, which you didn't seem to understand when we discussed Thm 3.13. If you agree with this, then we have nothing to argue about. That said, it's of course true that the letter f has lexical scope in the statement of IVT. That's why when we write f(e) = 0, we know what set f refers to: the one we started with when we said "Given f". 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.] You've never given any evidence I made any such error. You did however seem misunderstand Schmidt's Thm 3.13, to which I return. You agreed once on cls with my restatement of Schmidt's Thm 3.13: Given functions f_ij...there exists a unique family of functions E_i ... such that E_i( Option_ij ) = f_ij ( E_ij1(S_ij1),..., E_ijk(S_ij{k_ij}) ) // Suppose we have some function E_i & f_ij that satisfy these Schmidt equations above. Apply Thm 3.13 to our functions f_ij. Thm 3.13 asserts that there exist a unique family of semantic functions. WHAT ARE THOSE SEMANTIC FUNCTIONS? It's obviously the E_i functions we started with. If you do agree that, we have nothing to argue about. If you don't agree that the 3.13-produced functions are the E_i started with, then you don't understand the pure Math world. Now if instead you want to say that the language "Given f_ij...there exists unique E_i ..." really means that the E_i are defined by structural induction, then again, you don't understand the pure Math world. You wouldn't say that about the IVT, right: IVT: "Given f ... there exist e ... such that f(e) = 0" That doesn't mean e is defined by structural induction, right? [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. Yeah, everyone understands that. 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.] Perhaps you just misunderstood me. I meant exactly what I just said above. If you agree with me above about my use above of Schmidt's Thm 3.13, then we're fine. [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 sure didn't know that! And you're right, I no absolutely nothing about constructive mathematics. All I've ever heard is that it's too weak to get anything done in. Do you actually want to work there? Has anyone written a point set Topology book using constructive math? And constructive math has N and power sets? My favorite set theory book (lost from the library, alas) by Just & Weese calls the power set axiom the other nonconstructive axiom. [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.] Perhaps this is all true. But why don't you just explain how you compute the subset in finite time curly-E[e] subset U x S x K x A Or at least say whether Stoy or some other book proves your result (which follows from this), that curly-E is a computable function. 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. Correct, by Goedel & Cohen's amazing work. By construction, we can tell the model that satisfies CH from the model that satisfies its negation. Yes, but it's irrelevant. Perhaps you missed the phrase "in the pure Math world". CH has no relevance to the pure Math world. Isn't that a strange fact? Perhaps you don't know what I mean by the pure Math world. I mean Topology, PDE, number theory, Algebra, except of course in cases where these subjects brush up against such independence results. Like the Whitehead conjecture in Algebra, I forget the statement, maybe Ext^1(G, Z) = 0 for any torsion free group, and it's independent because of really huge G? That's not part of the pure Math world :) 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.] Sounds like real confusion on your part about the pure Math world. How do you think the pure Math world works? Pure mathematicians publishing papers in respectable journals, say the Annals of Math, what logical framework do you think they work in? Constructivism, axiomatic ZFC proofs? I say that pure mathematicians work with "actual" sets, which they "know" to be elements of some model of ZFC, and their constructions, theorems & proofs of our pure mathematicians *ought* to be justified by Halmos's book, but in practice, our pure mathematicians (including me) don't understand this formalizability.