Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 29 Sep 2006 17:33 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 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 What about it? There's no formal derivation of a result from Computer Science in this book. > 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 There's no formal derivation of a result from Computer Science in this book either. > 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. No you didn't. You never gave a formally derived result from Computer Science. > 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. :-) Since you haven't given a reference to a formally derived result of Computer Science, you have substantiated my original claim. But why did you claim that such a result existed? C-B > 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 29 Sep 2006 17:38 Steven Zenith wrote: > Charlie-Boo wrote: > ... > > > 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. > > Which only shows us that I am a prophet. You have not read beyond the > cover. That's not true. I read the whole thing. It doesn't show any formally derived result from Computer Science. Your claim that such a result exists is false. C-B > With respect, > Steven
From: Charlie-Boo on 29 Sep 2006 17:44 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. No you didn't. You only claimed that you did. > > 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. Yes I did. I read it and it doesn't contain what you say. What more am I supposed to do? > 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 - Your premise is not true. There is nothing to acknowledge. I "acknowledge" it by pointing out that fact that the result we discussed (a formally derived result from Computer Scuience) does not appear in that reference, despite your claims to the contrary. > 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. No, it contains no such result. You can say it as often as you want, but it is still a false statement. C-B > With respect, > Steven
From: Charlie-Boo on 29 Sep 2006 17:55 Steven Zenith wrote: > 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. You didn't read it enough to understand it, but you are claiming that you were "courteous" by not summarily dismissing it? Summarily dismissing something you never actually read would be the height of folly. How can you claim professionalism due to your not committing such a frivolous act? Your standard of excellence for yourself is exceedingly low. > I have no doubt that you will not be able to contain yourself before you > review the above references. :-) You just admitted that you did not take the time to even tell if my reference makes sense or not, so you are the one who cannot contain himself before reviewing the reference. You did so in reality, while your claim that I do so is only a conjecture. C-B > With respect, > Steven
From: george on 30 Sep 2006 11:45
> george wrote: > > Godel's original proof was a formal derivation. Peter_Smith wrote: > No it wasn't. Gödel's original proof was a bit of informal > mathematics. He *claimed* in 1931, at the end of his great paper, that > the informal reasoning could be carried out within the formal > type-theory he labels P. But he didn't show it there. It belatedly occurs to me that I could spare myself some of this embarrassment just by reading far enough back in THIS newsgroup. In sci.logic in 1997, Marv Schlottman went all the way back to the source: > In the article "Ueber formal unentscheidbare Saetze der > Principia Mathematica" ("On formally undecidable propositions > of Principa Mathematica") in Monatshefte fuer Mathematik 38 (1931) 173-198, > Goedel writes on page 197: "Saemtliche in Abschnitt 2 und Abschnitt 4 bisher definierte Begriffe (bzw. bewiesene Behauptungen) sind auch in P ausdrueckbar (bzw. beweisbar)." ("All concepts (propositions, resp.) which are defined (proven, resp.) so far in Section 2 and Section 4 are also expressible (provable, resp.) in P.") > Section 2 of this article contains the construction of the famous proposition > 17 Gen r" and the proof that this proposition cannot be proven or refuted > in P (the formal system of number theory Goedel considers), provided > P is omega-consistent (later on, B. J. Rosser extended this theorem > assuming only consistency). > Therefore, although you are right if you say that Goedel presented his > argument informally (and we are lucky that he did so), Goedel himself > emphasized that his proof of the incompleteness theorem can carried out > in the very formal system of number theory whose incompleteness it > states. .... > BTW, there _are_ "a good many people" who haven't understood this > point, but, as shown, this does _not_ include Goedel. |