Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 4 Oct 2006 23:35 Steven Zenith, Charlie-Boo wrote: > > What publication and page number contains the formal representation > > of a result from Computer Science and its formal derivation that you > > have been touting for weeks? > > an ACM paper by Geof Barrett, as I recall. The paper is titled, "Formal Methods Applied to a Floating-Point Number System". But what do they accomplish in this paper? What is the Computer Science result that is formally derived? There is none. Is this why you don't give the page number: because there is no such page? They describe a notation for specifying properties of real number arithmetic on a computer: the size of the storage used to represent the real number, the rounding algorithm, the arithmetic operations available. They say that they want to be able to prove properties of it and generate programs that perform these operations. But they don't accomplish any of this. At four points they give expressions and state that earlier expressions can be transformed into them. At the end they say "Now the components of the decomposed specification may be transformed into implementations independently to each other in a similar manner." This does not specify any result from Computer Science or how to formally derive it. It is merely a series of expressions without showing that it has any significance. They don't prove anything. There are no theorems. No conclusions or programs or anything else with meaning is derived. There are no axioms, rules of inference, or any other system for deriving anything. All they give is a series of expressions that are supposed to represent the above characteristics of the hardware and the final vague assertion quoted above. What have they proven? I asked for a result from Computer Science that is formally derived. This paper does not contain any theorems, nothing is derived, and no method of deriving anything is presented. It has none of what I described. I will email a copy of the paper to anyone who requests it, using the Reply to Author emailing feature of Google Groups (just don't tell the publisher.) In stark contrast, my ARXIV paper contains the formal derivation of four programs (from two specifications) and four theorems from the Theory of Computation, with detailed, precise, completely formal lists of: 1. Axioms for Number Theory, Database retrieval and Theory of Computation (section IV, V, VI.) 2. Rules of Inference for all 3 areas (section III. Rules of Inference) 3. Derivation of two programs to decide if one number is a factor of another number (section IV. An Example from Number Theory). 4. Derivation of two programs to list all employees who earn more than their manager (section V. An Example from Database Retrieval.) 5. Derivation of four theorems from the Theory of Computation: The set of Turing Machine that halt no on themselves is recursively enumerable, the Membership Problem is unsolvable, the Self-applicability Problem is unsolvable, and the Halting Problem is unsolvable (section VI. An Example from the Theory of Computation, and section VII. Unsolvable Wffs.) For each result, I give the formal steps. Each step is an axiom from (1) or a previous line and a Rule of Inference from (2) that applies to it to produce the current line. The last line is the theorem. (We also reverse the process to show how to prove a given theorem.) The theorem is either the representation of a computer program, or a theorem from the Theory of Computation. The results and the steps used to derive each are plainly shown in complete detail. I will answer any questions that anyone has as to how it works. See http://arxiv.org/html/cs.LO/0003071 Now I ask: Who else has done anything like that? Where are specific, detailed, formal theorems and their derivations? C-B > With respect, > Steven
From: Charlie-Boo on 24 Oct 2006 13:03 H. J. Sander Bruggink Charlie-Boo Steven Zenith: > >> It cannot have been peer reviewed. > > That conjecture - even if true - has no relevance to anything that we > > have discussed. > Of course it's relevant. Errors are sometimes made, > obviously, but in general papers in peer reviewed journals > and conference proceedings are of higher quality than > than an obscure Arxiv paper. "Inventions rarely come from people within an industry, but, instead come from people on the outside who aren't under the same limiting beliefs & habitual thinking that forms within any organization or industry. - Dr. James Asher, San Jose State University, "On Advanced Learning" > groente > -- Sander
From: Brian on 31 Oct 2006 21:24 > "Inventions rarely come from people within an industry, but, instead > come from people on the outside who aren't under the same limiting > beliefs & habitual thinking that forms within any organization or > industry. - Dr. James Asher, San Jose State University, "On Advanced > Learning" Sounds nice, but complete B.S. Here's a "top ten" list from the U.S. Patent Office. ( year 2004 ) Doesn't read like a list of "outsiders" to me. http://www.uspto.gov/main/homepagenews/bak11jan2005.htm
From: Charlie-Boo on 6 Nov 2006 09:47
Brian wrote: > > "Inventions rarely come from people within an industry, but, instead > > come from people on the outside who aren't under the same limiting > > beliefs & habitual thinking that forms within any organization or > > industry. - Dr. James Asher, San Jose State University, "On Advanced > > Learning" > > Sounds nice, but complete B.S. How about Cantor? Godel (vs. Hilbert)? "The world is flat." et. al.? > Here's a "top ten" list from the U.S. Patent Office. ( year 2004 ) > Doesn't read like a list of "outsiders" to me. > > http://www.uspto.gov/main/homepagenews/bak11jan2005.htm That's by frequency, not innovativeness. So naturally the Conservative mainstream big corporations are listed - IBM et. al. The outsider is small and can't do the quantity, but what is the quality of the mainstream Conservatives? A mountain of junk isn't worth an ounce of quality. For example, Peano's Axioms require 5 complex expressions in mainstrream Mathematics, but only a single trivial Axiom in CBL: TRUE(x). Rebel Occam showed that such simplifications are always the best way to formalize anything. C-B |