Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 17 Sep 2006 01:19 Jan Burse wrote: > 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. Have you given a method for automatically determining the result of running a given program? I know not. The user has to enter in the conditions at each step and all the system does is to "verify" that the expressions entered have the legal format of an expression and are compatible with each other. The system doesn't figure out ANYTHING. This is typical of the bullshit that peope write. The Curry-Howard "Program Synthesis" system requires you to type in the command/argument expressions that are combined to form the program. Likewise, your "Program Verification" requires the user to type in the conditions that describe the behavior of the program. In a true Program Synthesis system, the user types in only the specification and the system creates the program. In a true Program Verification system, the user types in only the program and the system creates the conditions that describe what the system does. Do you know of any system that does this? I know of one system that does. I have given it with examples. Can you give examples of what you claim? No. Why? Because you are a big liar. Give an example if you are right and I am wrong. Don't give any examples if I am right and you are a liar. There's no reason to believe unsubstantiated statements. The only possible reason for someone to go on and on with claims and not give any examples to substantiate it is that he is just a liar. C-B > 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: zzbunker@netscape.net on 17 Sep 2006 01:47 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. Programs that output themselves are quite trivial, since it's what the assembler instruction NOP does, Which isn't the same thing as programs that copy themselves. > 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 17 Sep 2006 01:54 Charlie-Boo wrote: > abo wrote: > > 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.) > > Here's one axiom from the Theory of Computation: > > YIT(I,J,K)* > > where YIT(a,b,c) means "Program a with input b halts yes at iteration > c." and the axiom states that (in standard terminology) the relation > YIT is recursive. > > You will find an analogous truth in many bases of computing (computer > programs and systems of logic.) Are you saying that this axiom is > bullshit? > I don't know what definition of "recursive" you are using - maybe you're using a non-standard definition (such as you were for "programming language" in another part of this thread). Whatever. The existence of a UTM is not intuitively obvious. Sorry, I don't want to waste more of my time. This is my last reply.
From: Charlie-Boo on 17 Sep 2006 11:47 zzbunker(a)netscape.net wrote: > 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. > > Programs that output themselves are quite trivial, > since it's what the assembler instruction NOP does, > > Which isn't the same thing as programs that > copy themselves. You are proving that there is a programming language in which there is a program that outputs itself, but the theorem is that there is such a program in all programming languages (C++, Algol, et. al.) C-B > > 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: Charlie-Boo on 17 Sep 2006 11:56
abo wrote: > Charlie-Boo wrote: > > abo wrote: > > > 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.) > > > > Here's one axiom from the Theory of Computation: > > > > YIT(I,J,K)* > > > > where YIT(a,b,c) means "Program a with input b halts yes at iteration > > c." and the axiom states that (in standard terminology) the relation > > YIT is recursive. > > > > You will find an analogous truth in many bases of computing (computer > > programs and systems of logic.) Are you saying that this axiom is > > bullshit? > > > I don't know what definition of "recursive" you are using - maybe > you're using a non-standard definition (such as you were for > "programming language" in another part of this thread). Whatever. Not so. A Programming Language is an r.e. set of expression and rules to map them onto the set of recursive functions. > The existence of a UTM is not intuitively obvious. Sorry, I don't want > to waste more of my time. This is my last reply. If a small well-defined set of axioms and rules can be used to generate the results of a theory, then they have captured the principles from which those results are constructed. If they don't seem "intuitively obvious" to someone, that doesn't change the fact that they are in fact the building blocks for creating those results. If they don't seem obvious to you, maybe you need to sudy the theory more. If you demand that more axioms be added to explain the first axioms, then you are unnecessarily expanding the size of the system. By Occam's Razor, the smaller set of primitives is preferred. C-B |