Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Patricia Shanahan on 3 Oct 2006 09:46 abo wrote: > Charlie-Boo wrote: .... >> What do you think about the rule that says the person making a claim >> has to present the proof here, not just give a reference and say that >> it's proven there? > > I don't agree with that rule. > >> Seems to me it would be a lot more efficient, >> everyone could see it instantly, it would eliminate wild goose chases. > > It may save you time, but it doesn't save the other person time. And - > perhaps this is hard for you to believe - the other person is likely to > consider his time as more valuable than your own, so from his point of > view there is no saving. > There are two additional issues: 1. Copyright. If the claim is the main result of a paper, posting the proof could amount to substantial republication of the paper, not just a fair use extract. 2. Formatting. A Usenet article should be plain ASCII. Mathematical proofs tend to be much more readable in systems that allow equation formatting. Patricia
From: Charlie-Boo on 3 Oct 2006 10:04 abo wrote: > I think you should just tighten - and > clarify - your claim with "no one has formally proved the theorem that > no program can compute the halting problem, in a system with > interesting axioms" (you need the latter to stop the rejoinder, > consider the system with the single axiom being the theorem itself). I think we can define "interesting". For example: 1. Infinite number of distinct theorems. 2. No axiom is used in only one (nonredundant) proof. 3. Includes these 10 theorems. 4. No more than 6 axioms. 5. No literals in the axioms. (Properties of my axioms.) Of course, the crooks will come up with another way to slip away. BTW That's the trick that TPTP.ORG uses - axioms hard-coded for each theorem. > On the other hand, I did my thesis under Roscoe and actually was one of > Roscoe's first grad students (maybe even his first, can't remember). > So I do agree with Steven. For instance, I would take program > verification as an example of a formal proof of a result in computer > science. > > {x = 0} if x = 0 then x = 1 else x = 2 {x = 1} > your view of "result" is more > limited than my own and this kind of thing only proves how a specific > program behaves. It's two different things - we need two different terms, not two definitions for one term. It's not what I described. See A-F in OP. It wasn't generated. I would appreciate an example of anything automated, very much. I wonder how to formally define both tasks: a reasonable axiomatization and tools for programmers (manual methods)? > > What do you think about the rule that says the person making a claim > > has to present the proof here, not just give a reference and say that > > it's proven there? > It may save you time, but it doesn't save the other person time. It saves every viewer tons of time. He wouldn't have to look up other people's citations. And it would disarm the liars and save the victims of BS citations. C-B Thanks for the non-political, non-hysterical, honest, thoughtful post!
From: Charlie-Boo on 3 Oct 2006 10:08 Patricia Shanahan wrote: > abo wrote: > > Charlie-Boo wrote: > ... > >> What do you think about the rule that says the person making a claim > >> has to present the proof here, not just give a reference and say that > >> it's proven there? > >> Seems to me it would be a lot more efficient, > >> everyone could see it instantly, it would eliminate wild goose chases. > There are two additional issues: > > 1. Copyright. If the claim is the main result of a paper, posting the > proof could amount to substantial republication of the paper, not just a > fair use extract. > > 2. Formatting. A Usenet article should be plain ASCII. Mathematical > proofs tend to be much more readable in systems that allow equation > formatting. Just summarize it, PLEASE. Everybody would save time, of course (unless one person cites more than everyone else combined.) And what is the value of justice? Computer systems are never written with intentional errors to save time, anyway. C-B > Patricia
From: H. J. Sander Bruggink on 3 Oct 2006 10:39 Charlie-Boo wrote: > H. J. Sander Bruggink wrote: >> Charlie-Boo wrote: >>> H. J. Sander Bruggink wrote: > >>>> Either your definition is wrong, or your inferences are >>>> wrong. > >>> No. Give an example. > >> Your "proof" of the halting problem. (Yes, I know this is >> because you try to sneak in some sort of reductio ad >> absurdum. But sneaking in inference rules hardly counts >> as "formalization".) > > What? There's something wrong with reduction ad absurdum?? Are you > crazy? Ok. Then your definition was wrong, because the last line of the proof is *not* the sought after theorem. Thanks for the clarification. [snip] >> Ah, you don't have an unrestricted loop? It's not even >> Turing complete, then? > > It sure is. You don't understand it. Read section II: "The > arguments to commands represent actual code in real life programming > languages that performs loops, variable assignment, conditional > execution and output." Programs are constructed from the fixed set > of primitive programs (axioms) that define the programming language, > which can be any program. (Besides, the command is FOR not WHILE.) Ok. So you *claim* that the language is Turing complete. Care to give a proof of that? And no, in general you need some sort of While to be Turing complete. With only FOR the language is only primitive recursive. Unless of course FOR is some sort of WHILE in disguise, such as in C-derived languages. But in your case, that doesn't seem to be the case. In any case, it's your job to show that the language is Turing complete, not mine to show that it isn't. (Some note about substantiating your claims seems to be in place here... :-) [snip] I quote this line for later use: > Why do you keep forgetting this is sci.logic not political.science? [snip] >> Because I have seen systems translate a proof to a >> program. > > That's not program synthesis. It's odd that you say that, because your system tries to do *exactly the same thing*: prove a formula, then automatically translate the proof into a program. Frankly, I don't care whether or not it's "program synthesis". The Coq people call it "program extraction", which is a better name. I just want that you require the same things from your own work as from the work of others. Did you already implement your system, btw? (No, I bet not.) > You are being fooled by the BSers. > The "proof" is not generated - the user enters it - and it's just > the program broken into pieces. (I explained that earlier. READ THE > LITERATURE.) You are only making a fool of yourself. Just look at the example I pointed you to in the "Turing vs Godel" thread. >>> And please, be a scientist: no reference to "generally" or prestige >>> or people's opinions (peer review), ok? > >> Charlie, I know that people's opinions of your paper >> are not that high. This is not because people have >> bad opinions, it is because you have a bad paper. > > Do I have to drag out my fan club membership list? > > That's just more stupid politics. More than half of Americans think > Saddam Heussein had weapons of mass destruction when we invaded. [quote from CB] Why do you keep forgetting this is sci.logic not political.science? [/quote] 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? [snip] groente -- Sander
From: Steven Zenith on 3 Oct 2006 11:36
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. You are enjoying my error, and I am happy for you, but it doesn't mean that much. > 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. With respect, Steven |