Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: hale on 3 Oct 2006 12:28 Charlie-Boo wrote: > Steven Zenith wrote: > > Charlie-Boo wrote: > > > > I gave a reference to my ARXIV paper a little earlier (and I believe > > > you and I have discussed it before, if I am not mistaken.) In any > > > case, here is the on-line version again: > > > > > > http://www.arxiv.org/html/cs.lo/0003071 > > > > I took a closer look at this and as far as I can tell it is nonsense. > > What part seems to be nonsense and why? I'd be glad to elaborate. In the section "IV. An example from Number Theory", you give the following definition: 4. MUL(a,b,c) , MUL(a,b,c) ^ ~LT(c,a) a * b > a This doesn't seem to be a definition of MUL(a,b,c). I find this confusing and misleading. Bill Hale
From: Charlie-Boo on 3 Oct 2006 13:01 H. J. Sander Bruggink wrote: > your definition was wrong, because the last line > of the proof is *not* the sought after theorem. Thanks for > the clarification. WADR, I think you're still confused. There are positive results, such as the construction of a computer program for practical purposes (Program Synthesis: Number Theoretic functions and DataBase Queries) or to show that it exists (the set of refutable sentences is r.e. and the Fixed Point Theorem). There are negative results (unsolvability of the Halting Problem and Paradoxes.) There are also two ways to generate a theorem plus proof: apply the rules to the axioms (Incompleteness in Logic Theorems), or work backwards from a given theorem applying the inverses of the rules (Program Synthesis.) So the theorem can be at either the beginning or the end. > you *claim* that the language is Turing complete. > Care to give a proof of that? 1. For any program: a. if it enumerates a set, then it is of the form: FOR (loop code) WRITE(x) b. if it decides a set, then it is of the form: IF (decision code) WRITE(TRUE) WRITE(FALSE) c. if it computes a function, then it is of the form: SET X=(function code) WRITE(X) qed > And no, in general you need some sort of While to be > Turing complete. With only FOR the language is only > primitive recursive. Good point except that you applied it wrong. If the FOR is of the form that computes Godel's primitive recursion, then it doesn't get you beyond Godel's primitive recursive functions/relations. But if you can increment by zero, then you can create a potential infinite loop and the number of iterations will be any recursive function of the inputs (the point at which you terminate the loop.) I think you still don't understand the language (not necessarily your "fault".) The argument to the FOR is any program segment that loops. The language is really a way to combine primitive programs (axioms), and represents these axiomatic programs plus control structures (implementable by any programming language.) For example, if you have a primitive program that loops through the natural numbers, call it AX1, then we FOR (AX1) and we have that loop in the program constructed. > Unless of course FOR is some sort > of WHILE in disguise, such as in C-derived languages. In disguise? You're thinking about that Zenith guy who plays the shell game: "Guess where the missing formalization is? In this reference? Nope, look again." > >> I have seen systems translate a proof to a program. Curry-Howard is not based on proofs and it is not automatic. They call it proofs, but it is not generated. They don't create programs from specifications. They (claim to) create programs from pieces of code that the user types in. It isn't proving anything. It isn't automatic. They never show how to create the input automatically. It is not program synthesis. Give an example of a program being created automatically using any system that is not a Computationally Based Logic. Nobody has. The fact that it can be done with a Computationally Based Logic and not by Curry-Howard shows they aren't the same thing. I did it and they didn't. There is no comparison. Give an example of a Proposition Based Logic being used for program synthesis. You can't. Trying to compare a Computationally Based Logic to a Proposition Based Logic shows that you don't understand one or the other (inclusive or.) > Did you already implement your system, btw? (No, I bet not.) Yes. I sell the output (Billing and Accounts Receivable Systems, Radiology Systems, etc.) to hospitals and health insurance companies. It is constantly running and making money for me, so I can post to Google Groups all day long. (How much was the bet?) Why do you think that Prof. Gio Wiederhold of Stanford invited me to represent the United States as a Computer Scientist in a cultural exchange with the People's Republic of China under the People to People program? > You are only making a fool of yourself. Just look at > the example I pointed you to in the "Turing vs Godel" > thread. Liar, you never gave me a pointer. (You didn't even sell me one.) > >>> And please, be a scientist: no reference to > >>> people's opinions (peer review), ok? > >> Charlie, I know that people's opinions of your paper > >> are not that high. You don't take orders very well, do you? > > That's just more stupid politics. More than half of Americans think > > Saddam Heussein had weapons of mass destruction when we invaded. > But apparently you think that more than half of Americans > are experts on weapons of mass destruction. Otherwise the > analogy would not really hold, would it? Well, George Bush has been explaining them to us for 5 years now. They have mobile biological weapons labs on carts that they kept in the desert (disguised as weather balloons.) READ THE LITERATURE (The Boston Globe.) C-B > groente > -- Sander
From: Charlie-Boo on 3 Oct 2006 13:25 Steven Zenith wrote: > Charlie-Boo wrote: > > Steven Zenith wrote: > > You wrote, "Since when is root 2 a real number?". After several people > > pointed out that the square root of 2 is in fact a real number, you > > replied, "the typing error is merely a matter of convention". What > > did you mean to type instead of "Since when is root 2 a real number?" ? > > I made a mistake and acknowledged it. I was drawing a type distinction > between rationals and irrationals - it is a distinction that occupies > me. I would advise you to spit it out if you can. > You are enjoying my error, and I am happy for you, but it doesn't > mean that much. Do I detect a bit of sarcasm dripping from your lips? It means that you don't know fundamentals of Mathematics, so all of your assertions are suspect. And you claim that people want to give you awards but you're too busy to accept them? What was the award for, Volunteer of the Week? > > Obviously Dedekind does not say anything contrary to the above facts > > nor does he answer my question concerning our conversation. > > Actually, I was rejecting your claim that reals have been around since > antiquity - you did not pick up the relevance of the reference, and are > compounding my own ignorance with yours. If you choose, we can both > look stupid here. So you admit that you're ignorant and stupid. Now please allow me to remove myself from your roster: Hippasus of Metapontum proved that the square root of 2 (the number you had so much trouble with) is irrational around 500 BC. That is the date that I was referring to. (Dedekind only attempted to formalize real numbers. If he were actually smart, he would have used a Computationally Based Logic, in which we can do this very easily: {T,F} => {T,F} Logic {T,F} => N Rationals N => {T,F} Reals (By Occam's Razor this is preferable.)) So, are you going to check yourself into a rehab? Congressman Foley knows of a good one. BTW 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? Your admirer, C-B > With respect, > Steven
From: Charlie-Boo on 3 Oct 2006 14:19 > > > > http://www.arxiv.org/html/cs.lo/0003071 > In the section "IV. An example from Number Theory", you give the > following definition: > > 4. MUL(a,b,c) , MUL(a,b,c) ^ ~LT(c,a) a * b > a > > This doesn't seem to be a definition of MUL(a,b,c). I find this > confusing and misleading. > > Bill Hale Thanks for the interest. DEF 4 states that MUL(a,b,c) is equivalent to MUL(a,b,c) ^ ~LT(c,a), but is not meant to capture enough information to completely define MUL. Note in section II: "DEF:P,Q means that wffs P and Q, using pseudo-variables a, b, c, ..., are equivalent by definition, and may be substituted for each other. (For example, the assertion that P is a subset of Q is represented by DEF:P,P^Q.)" and here "Universal Set: { 1, 2, 3, ... }". Then DEF 4 is MUL(a,b,c) <=> MUL(a,b,c)^~LT(c,a) MUL(a,b,c) => ~LT(c,a) a*b=c => ~(c<a) ~(a*b < a) ~(b<1) DEF 4 is used in step 12 in the first construction of a program to decide if one given number is a factor of another. C-B
From: Bill Hale on 3 Oct 2006 14:47
In article <1159899594.291222.133100(a)i3g2000cwc.googlegroups.com>, "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > > > http://www.arxiv.org/html/cs.lo/0003071 > > > In the section "IV. An example from Number Theory", you give the > > following definition: > > > > 4. MUL(a,b,c) , MUL(a,b,c) ^ ~LT(c,a) a * b > a > > > > This doesn't seem to be a definition of MUL(a,b,c). I find this > > confusing and misleading. > > > > Bill Hale > > Thanks for the interest. DEF 4 states that MUL(a,b,c) is equivalent to > MUL(a,b,c) ^ ~LT(c,a), but is not meant to capture enough information > to completely define MUL. But, you are not saying that the two are equivalent. You are saying that the two are equivalent *by definition*. This is confusing. You are misusing the word "definition". Bill Hale |