Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 16 Sep 2006 12:10 Steven Zenith wrote: > Jack Campin - bogus address wrote: > >... > > So you just add a second argument to the sqrt function saying how many > > places of precision you want. That two-argument function does terminate, > > and there's no implementation dependence about it. > > Well, you have now placed the implementation dependence in the new > argument. Why is there implementation dependence in writing a program to calculate square root to a given number of places? We simply perform the calculation for the specified number of digits. (If they ask for tons of digits, then we keep them in an array of digits and perform the calculations on the array.) In fact, how could any exact specification be implementation specific? If it can be implemented on one computer/programming language, then obviously it can be implemented on all of them, as all programming languages (meaning e.g. C++, Algol, etc.) implement the same functions. Again you are confusing ill-written (e.g. incomplete) specifications with theoretical aspects of Computer Science. You are good at name dropping and referring to awards and organizations, but your technical statements are unsubstantiated and show a very immature understanding of both Mathematics (as regards the concept of a function) and programming (as regards what can be implemented.) C-B > It is better to explicitly express a pragmatic, I agree, but > these pragmatics will play hell with the formal system unless > differentiated from the algorithmic goals. > > With respect, > Steven
From: Charlie-Boo on 16 Sep 2006 12:24 abo wrote: > I'm interested in the axioms you need to prove Godel's first > Incompleteness Theorem (in 10 steps). Please include the statement of > the Theorem in your system, as well as an explanation of any > idiosyncratic symbolism. Great! (These are good questions as well.) Ok, how about if you start a new thread that asks for the above and post the subject here (or I'll just see it myself.) A deal? > I thought your claim was that your axioms are "intuitively obvious". They are. You mean that it's not intuitively obvious that a UTM exists? Maybe not to us, but ask a child of the computer age if there are programs that run programs. The tottlers will ask you if you prefer Windows or UNIX. C-B
From: Jan Burse on 16 Sep 2006 12:46 Hi Charlie-Boo wrote: > Jan Burse wrote: >>For a start, try: >> Thompson, S.: Type Theory and Functional Programming, >> Addison-Wesley Publishing Company, 1991 >> >> He gives a definition of quicksort and then >> proofs its termination and correctness. Did you read the reference. I believe not. I should have mentioned: He gives a proof system based on type theory and functional programming for proofing termination and correctness of programs. He then gives as an example instance of his proof system a definition of quicksort ... To show termination and correctness the proof system makes use of induction proofs. So its not what you describe below. It is on the contrary a proof system which can be mechanized, and not a manual informal example. > The only difference is that the articles spell out exactly how > it is verified: "Consider variables A and B. Note that at every > point A<B. Now, also note that every iteration through > this loop decreases B. . . ." Bye
From: Jan Burse on 16 Sep 2006 12:49 Hi BTW, from descriptive complexity theory it should be clear that one can proof termination of programs. For example if a program is in P, then you have a polynomial upper bound for the number of steps the programm does. And so on, all the complexity classes below the kleene hierarchy imply their own upper bound. Unfortunately how this is related to correctness of a program I cannot recall at the moment. Google for: Descriptive complexity. Bye Jan Burse wrote: > For a start, try: > > Thompson, S.: Type Theory and Functional Programming, > Addison-Wesley Publishing Company, 1991 > > He gives a definition of quicksort and then > proofs its termination and correctness. > > From this follows that one can in theory also > do programm synthesis: > > Just generate programms and pick those > that you proofed termination and correctness. > > But there are some interesting approaches in > inductive logic programming to do synthesis. > Try googling the terms "machine learning" and > "inductive logic programming". > > Bye > > Charlie-Boo wrote: > >> Do we all agree that Computer Science definitely should be formalized? >> >> While the definitions of common terms (e.g. recursively enumerable) are >> formal, the manipulations of these concepts (e.g. the derivation of >> proofs) is not. Can anybody show a single example of a formal >> derivation of a result from any branch of Computer Science? For >> example: >> >> 1. Program Synthesis: The creation of a computer program based on only >> its specifications. >> >> 2. The Theory of Computation: A formal derivation of Turing's proof >> of the unsolvability of the halting problem. >> >> 3. Recursion Theory: A formal proof that there is a program that >> outputs itself, or of the Fixed Point theorem or the Recursion theorem. >> >> 4. Incompleteness in Logic: A formal derivation of Godel's >> Incompleteness theorems or Rosser's improvement or Smullyan's Dual >> Form theorem. >> >> Any formalization would include: >> >> A. A formal statement of the theorem or result. >> B. The meaning of any such statement. >> C. How A corresponds to the statement of the theorem. >> D. An algorithm for generating formal statements such as A. >> E. A demonstration that D generates A. >> F. A demonstration that D generates only true statements. >> >> Curry-Howard, Manna/Waldinger, Boyer/Moore, Modal Logic, Prologue and >> TPTP all attempt to do this, but nobody has ever shown any examples of >> anything near A-F. >> >> Would we say that formalization is the ultimate goal of every branch of >> Computer Science? What problem is not enhanced when expressed >> formally? >> >> C-B >>
From: abo on 16 Sep 2006 13:03
Charlie-Boo wrote: > abo wrote: > > > I'm interested in the axioms you need to prove Godel's first > > Incompleteness Theorem (in 10 steps). Please include the statement of > > the Theorem in your system, as well as an explanation of any > > idiosyncratic symbolism. > > Great! (These are good questions as well.) Ok, how about if you start > a new thread that asks for the above and post the subject here (or I'll > just see it myself.) A deal? > > > I thought your claim was that your axioms are "intuitively obvious". > > They are. You mean that it's not intuitively obvious that a UTM > exists? Maybe not to us, but ask a child of the computer age if there > are programs that run programs. The tottlers will ask you if you > prefer Windows or UNIX. I'm afraid that's more bullshit. (That = "They are" and the explanation you give.) > > C-B |