Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 21 Sep 2006 15:10 Steven Zenith wrote: > Charlie-Boo wrote: > > Steven Zenith wrote: > > > > > http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=65476 > > > > This is only an abstract. > > > > What is the theorem? > > What is the formal representation of the theorem? > > What is the sequence of steps (or at least the first few and the last > > few) that construct the formal representation of the theorem? > > > > I did give the answers to these questions. > > > I have given examples of CBL proofs. I continue to offer to present > > here the formal derivation of any of the theorems that I have mentioned > > and other related theorems that anyone wants: Godel 1931, Rosser 1936, > > Turing 1937, Kleene 1950's, Smullyan 1960-2000, Program Synthesis of > > Number Theoretic functions. > > > > Why don't you? > > Because that is not my level of participation here. You made a claim > and I pointed you to work that I believed countered the claim - you > have not, to my satisfaction, acknowledged the information I provided. > The derivations you are interested in do not seem to me to be > particularly interesting from a practical point of view, though as > examples that are case studies in CBL they are no doubt of interest. > > Why is it you have such a hard time acknowledging the work of others - > and I am not referring to my part in any of it - which was minor > compared to the people that established the formal basis of concurrency > theory (Roscoe, Hoare, Milner). The work speaks for itself and > directly contradicts your claim that CS has not been formalized in any > part. Why do you suppose that people claim "It's already been done.", then sometimes give a reference, but when you look, the reference doesn't contain what they say it does? And then when you ask them to just say what it is that they think the reference contains, they simply repeat the reference and say it's the other person's responsibility to prove their point? This is NOT how references are used in scholarly papers. In a published work, the author gives the result and then cites the original source of the idea, if the reader is interested in further information. They don't say "So-and-so proved a theorem. To find out what the theorem is and how he did it, refer to the reference." It seems that some unscrupulous people misuse references, as a means of both making an unsubstantiated claim and also as a barrier to communication rather than a vehicle. What do you think of someone who would do that? BTW Did you read the ARXIV paper on CBL? What did you think? Pretty amazing, isn't it? C-B > With respect, > Steven
From: Steven Zenith on 22 Sep 2006 02:46 Charlie-Boo wrote: > BTW Did you read the ARXIV paper on CBL? What did you think? Pretty > amazing, isn't it? Well, no. Not really. Not at all in fact. It's not original by any means - I haven't spent sufficient time with it to judge its quality - but again I'll refer you to the literature where more extensive treatments of these questions are given. Further, despite your claims, you have added nothing to our understanding of Computer Science theory. And I have given you the courtesy of finding and reading your reference. Find a library ... and turn your hearing aid up. :-) With respect, Steven
From: Charlie-Boo on 22 Sep 2006 08:30 Steven Zenith wrote: > Charlie-Boo wrote: > > BTW Did you read the ARXIV paper on CBL? What did you think? Pretty > > amazing, isn't it? > > Well, no. Not really. Not at all in fact. It's not original by any means. You mean that what some people have called nonsense was standard doctrine all this time? Wow! I am very interested in your findings. Where can I read more about the principles of CBL in the published literature? > - I haven't spent sufficient time with it to judge its quality - I thought you said it was already published? Where did you see it published? > but again I'll refer you to the literature where more extensive > treatments of these questions are given. You refer me to which literature? Did I miss something? (We already established that your links don't lead to any formal derivations of any Computer Science results.) > Further, despite your claims, you have added nothing to our > understanding of Computer Science theory. How about the following proof of Rosser's 1936 extension to Godel's incompleteness theorems that was formally generated by CBL: "If a system is consistent and complete, then the refutable sentences coincide with the unprovable ones, but the former is an r.e. set while the latter is not." Note that this result from Proof Theory is expressed entirely in terms of Theory of Computation and Propositional Calculus results. Have you ever seen such a short, simple proof of this important result? And do you know what Occam's Razor says about that? (I'm sure that a scholar such as yourself is aware of, and appreciates, these well-established principles.) > And I have given you the courtesy of finding and reading your reference. > > Find a library ... and turn your hearing aid up. :-) Ok. I live a few blocks from Harvard McKay library and 2 T stops from MIT Barker library. What article shall I look up that already contains CBL? Hey, I just thought of a good idea. Why don't you simply tell us all a result from Computer Science that has been formally generated (without human intervention)? You know, what is the theorem, its formal representation, and its formal derivation? That should only take a few minutes. Then we can reduce this discussion of dozens of claims to a single instance of substantiating those claims - a reduction in size of about 90%. I'm sure that Occam would appreciate that as well. And didn't your Mom and Dad teach you that it's not nice to make up stories? C-B > With respect, > Steven
From: Steven Zenith on 22 Sep 2006 10:54 The quality I refer to is the quality of the paper you have referenced - it would take some time to determine if what you have there actually makes any sense at all. It is not time that I am prepared to commit, but I do you the courtesy of not summarily dismissing it. What I saw there reminded me of Robin Milner's CSS. When you get to the library ask for this book: http://www.amazon.com/Communication-Concurrency-Prentice-International-Computer/dp/0131150073/sr=8-1/qid=1158936360/ref=pd_bbs_1/002-2129589-0385604?ie=UTF8&s=books And while you are at it ask for the reference I gave you in the first place: http://www.amazon.com/Theory-Practice-Concurrency-W-Roscoe/dp/0136744095/sr=1-2/qid=1158936562/ref=sr_1_2/002-2129589-0385604?ie=UTF8&s=books As to you other comments I will confess to being mystified. I have in previous postings complied with you request to state the theorem, formalism and technique of proof. The specific example, a case study, demonstrated the general case for the formal methods tools we used. Now that is it from me on this subject. Please have the last word, I have no doubt that you will not be able to contain yourself before you review the above references. :-) With respect, Steven Charlie-Boo wrote: > Steven Zenith wrote: > > Charlie-Boo wrote: > > > BTW Did you read the ARXIV paper on CBL? What did you think? Pretty > > > amazing, isn't it? > > > > Well, no. Not really. Not at all in fact. It's not original by any means. > > You mean that what some people have called nonsense was standard > doctrine all this time? Wow! > > I am very interested in your findings. Where can I read more about the > principles of CBL in the published literature? > > > - I haven't spent sufficient time with it to judge its quality - > > I thought you said it was already published? Where did you see it > published? > > > but again I'll refer you to the literature where more extensive > > treatments of these questions are given. > > You refer me to which literature? Did I miss something? (We already > established that your links don't lead to any formal derivations of any > Computer Science results.) > > > Further, despite your claims, you have added nothing to our > > understanding of Computer Science theory. > > How about the following proof of Rosser's 1936 extension to Godel's > incompleteness theorems that was formally generated by CBL: > > "If a system is consistent and complete, then the refutable sentences > coincide with the unprovable ones, but the former is an r.e. set while > the latter is not." > > Note that this result from Proof Theory is expressed entirely in terms > of Theory of Computation and Propositional Calculus results. > > Have you ever seen such a short, simple proof of this important result? > And do you know what Occam's Razor says about that? (I'm sure that a > scholar such as yourself is aware of, and appreciates, these > well-established principles.) > > > And I have given you the courtesy of finding and reading your reference. > > > > Find a library ... and turn your hearing aid up. :-) > > Ok. I live a few blocks from Harvard McKay library and 2 T stops from > MIT Barker library. What article shall I look up that already contains > CBL? > > Hey, I just thought of a good idea. Why don't you simply tell us all a > result from Computer Science that has been formally generated (without > human intervention)? You know, what is the theorem, its formal > representation, and its formal derivation? That should only take a few > minutes. > > Then we can reduce this discussion of dozens of claims to a single > instance of substantiating those claims - a reduction in size of about > 90%. I'm sure that Occam would appreciate that as well. > > And didn't your Mom and Dad teach you that it's not nice to make up > stories? > > C-B > > > With respect, > > Steven
From: Charlie-Boo on 22 Sep 2006 13:03
Steven Zenith wrote: > The quality I refer to is the quality of the paper you have referenced > - it would take some time to determine if what you have there actually > makes any sense at all. It's of high quality but not might make any sense? In other words, you judge it based on how it looks, although from a mathematical point of view it might be meaningless. Ah Ha! Now I see how you make your appraisals. Me, I always look for the mathematical content. No wonder we disagree so often. Really. > What I saw there reminded me of Robin Milner's CSS. When you get to the > library ask for this book: > > http://www.amazon.com/Communication-Concurrency-Prentice-International-Computer/dp/0131150073/sr=8-1/qid=1158936360/ref=pd_bbs_1/002-2129589-0385604?ie=UTF8&s=books > > And while you are at it ask for the reference I gave you in the first > place: > > http://www.amazon.com/Theory-Practice-Concurrency-W-Roscoe/dp/0136744095/sr=1-2/qid=1158936562/ref=sr_1_2/002-2129589-0385604?ie=UTF8&s=books That's a model for concurrency and synchronization, not program construction, much less does it show how to formally derive programs. > I have in > previous postings complied with you request to state the theorem, > formalism and technique of proof. The specific example, a case study, > demonstrated the general case for the formal methods tools we used. [ Does anybody know what he's talking about? Does anybody see any formal representation of a theorem and its derivation among these posts? ] It's a shame you can't give the actual formalisms here - or a link to where you supposedly gave it before. > Now that is it from me on this subject. Please have the last word, I > have no doubt that you will not be able to contain yourself before you > review the above references. :-) There's a lot of things you seem to know without proof. Prophesy might as well be one final example. Any tips on which stocks I should buy? It would be a way to compensate me for the time I wasted looking at the bogus references. Maybe a rule that there was some sort of penalty imposed of the one who makes the bogus reference, as a way to discourage dishonest people from using that tactic. My idea is that they be required to present the evidence within the current forum. Just a pipedream. C-B > With respect, > Steven |