Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 3 Oct 2006 05:31 Steven Zenith wrote: > Charlie-Boo wrote: > > > No, it wasn't in reference to your work or "types". It was in > > reference to established mathematics that has existed since antiquity. > > Now we are just compounding our ignorance - ask Dedekind. 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?" ? Obviously Dedekind does not say anything contrary to the above facts nor does he answer my question concerning our conversation. (Once again you give an irrelevant reference, not being specific as to where in the reference there is material of relevance or how it is relevant.) Your friend, C-B > With respect, > Steven
From: abo on 3 Oct 2006 07:18 Charlie-Boo 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?" ? > CBO - "type" not in the sense of hitting the keyboard, but "type" in the sense of computer languages, where it means something like "category" and the type of a variable could be an integer, or a real, or a double,... Apparently Steven uses idiosyncratic typing in his work - nothing wrong with that - he just forgot that the world doesn't share the same categories as he when he posted.
From: H. J. Sander Bruggink on 3 Oct 2006 07:18 Charlie-Boo wrote: > H. J. Sander Bruggink wrote: >> * You define inferences/proofs to be sequences of formulas, >> following from earlier formulas, and ending in the sought >> after theorem. Yet, in many of your examples, the last >> formula doesn't even resemble the sought after theorem. >> 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".) [snip] >> * It is not immediately clear to me what the computational >> power is of that toy language of yours is. > > Look at the example programs and those constructed. Do you doubt that > they calculate what I say? > >> In particular >> I have doubts about the fact that IF and WHILE clauses >> explicitly transfer control to the next line, which makes >> combining these control words problematic. > > They don't and there is no WHILE. Ah, you don't have an unrestricted loop? It's not even Turing complete, then? > >> * Your method is to prove a specification, and then >> transform that proof into a program. This is not a novel >> path. > > No. It is novel because it works. It is not a proof of a statement. > It follows the form of a proof (Axioms and Rules) and you prove that > the resulting program satisfies the specification. But people (e.g. > Curry-Howard) who say that you can construct programs by proving > (aX)(eY)R(x,y) where R(x,y) means input x produces output y in the > specification, are wrong. Unsubstantiated. > I don't use anything at all like that. > And mine works and theirs doesn't. > > And again we are back to the point where NOBODY EVER GIVES ANY EXAMPLES > OF THEIR SYSTEM SYNTHESIZING ANY PROGRAMS. (Excuse me for shouting, > but people always ignore that fact - which is the whole problem: > produce the program, already.) I did give an example a few weeks ago in a different thread (I think the "Turing vs Godel" thread), creating a program that mirrors a binary tree in a *real* *programming* *language* (OCAML). You chose to ignore that example, of course. > >> Yet, you don't even mention earlier comparable >> work. Yes, I know you think your work is superior, >> but if you want people to accept it, you have to >> write *in your paper* why that is so. > > Because nobody has shown a Program Synthesis system before. ... [snip] I said: "IN YOUR PAPER". I already know your many misconceptions, I'm not going to respond to them again. [snip] >> 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. > > That is meaningless. That is just their opinion. Yes, it's their opinion. Why is the opinion of knowledgable people meaningless? If some person who knows a lot about a specific field thinks an article in that field is good, then I am more inclined to read it, and usually with good reason. > This is SCIENCE. No, in your case it's just shouting nonsense. > "in general", "higher quality", "obscure" - what do they > mean? Buy a dictionary. > Not that I really have to engage in this meaningless point, but > do you realize how many errors there are in Turing's 1937 paper? > > The best thing you can do is to explain: > > Why do you believe that a Program Synthesis system has been produced > outside of CBL? Because I have seen systems translate a proof to a program. In particular, I have seen Coq do it. And I actually saw those produced programs *run* on an *actual computer*. Google for "program extraction". > > 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. [snip] groente -- Sander
From: abo on 3 Oct 2006 08:46 Charlie-Boo wrote: > > BTW If you have all the answers (an obvious extrapolation), then where > is the Computer Science result that is formalized - its formal > representation and its formal derivation? THAT I'd be interested in. > He won't even tell me the page it's on, much less present it here. >From what I've read you have a view of "computer science result" which is more limited than my own. 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). This may or not be true - I personally don't know. 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 is 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} and so forth. If you're interested I'll try to post a longer example tonight - it is step-by-step like a formal axiom system. But I imagine you are not interested, since again your view of "result" is more limited than my own and this kind of thing only proves how a specific program behaves. > > 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.
From: Charlie-Boo on 3 Oct 2006 09:20
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? Sneak it in? Read the line above the first proof above the HP: "if P => Q and -Q then -P". I use 8 rules for Program Synthesis (both Number Theoretic functions and DataBase retrieval) and a 9th rule for Theory of Computation (incompleteness results.) What's wrong with that? My definition isn't wrong and my inferences aren't wrong. Admit it. (Just say "Sorry, that was really stupid of me. Do you forgive me?". We'll all understand.) > >> I have doubts about the fact that IF and WHILE clauses > >> explicitly transfer control to the next line, which makes > >> combining these control words problematic. > > > > They don't and there is no WHILE. > > 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.) > > It is novel because it works. It is not a proof of a statement. > > It follows the form of a proof (Axioms and Rules) and you prove that > > the resulting program satisfies the specification. But people (e.g. > > Curry-Howard) who say that you can construct programs by proving > > (aX)(eY)R(x,y) where R(x,y) means input x produces output y in the > > specification, are wrong. > > Unsubstantiated. Curry-Howard being a Program Synthesis system is unsubstantiated, yes. What else is? > I did give an example a few weeks ago in a different > thread (I think the "Turing vs Godel" thread), creating > a program that mirrors a binary tree in a *real* > *programming* *language* (OCAML). > > You chose to ignore that example, of course. Maybe I slept through that one. Gimme a pointer. I'll prove it BS. No problem. > >> Yet, you don't even mention earlier comparable > >> work. Yes, I know you think your work is superior, > >> but if you want people to accept it, you have to > >> write *in your paper* why that is so. > > > > Because nobody has shown a Program Synthesis system before. ... > I said: "IN YOUR PAPER". My paper gives a complete list of all existent Program Synthesis systems. Anything else needed? > >> 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. > > > > That is meaningless. That is just their opinion. > > Yes, it's their opinion. Why is the opinion of > knowledgable people meaningless? Why do you keep forgetting this is sci.logic not political.science? > If some person who knows > a lot about a specific field thinks an article in that > field is good, then I am more inclined to read it, and > usually with good reason. What does that got to do with anything? > > This is SCIENCE. > > "in general", "higher quality", "obscure" - what do they > > mean? > Buy a dictionary. I can't find them anywhere. I looked in Barron's Dictionary of Mathematical Terms and CB's Encyclopedia of All Things Mathematical (both standard references.) > > Why do you believe that a Program Synthesis system has been produced > > outside of CBL? > > Because I have seen systems translate a proof to a > program. That's not program synthesis. 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.) > > 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. "The skeptic will say, 'It may well be true that this system of equations is reasonable from a logical standpoint, but this does not prove that it corresponds to nature.' You are right, dear skeptic. Experience alone can decide on truth." - Albert Einstein Einstein likes me. (Do you know what he's talking about? EXAMPLES!) "Great thinkers have always encountered violent opposition from mediocre minds." - Albert Einstein You know, your complaints are basically irrelevant. The only thing that matters is whether it meets the specs or not. What is the input and the output? Answer: A Predicate Calculus wff and a Computer Program, respectively. How it performs its magic is irrelevant (as long as there isn't a midget hidden in the box [no offense to Little People].) The truth of the matter is, nobody else has ever shown a way to create computer programs from their specs (no extra input needed.) I suspect there is no other way. It's all a matter of how programs are constructed - the properties of the recursive functions. Godel showed it first in 1931 ("primitive recursive") and CBL (Program Synthesis application) is based on those same rules. C-B > groente > -- Sander |