Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Patricia Shanahan on 13 Sep 2006 11:41 Patricia Shanahan wrote: > Phil Carmody wrote: >> Patricia Shanahan <pats(a)acm.org> writes: >> >>> Charlie-Boo wrote: >>>> Alec McKenzie wrote: >>>> >>>>> In which case you must have meant to say "A formal proof that in >>>>> every programming language there is a program that outputs >>>>> itself". >>>>> >>>>> It seems clear to me that that cannot be true >>>> Why? >>> Consider, for example, an XML-based Turing Machine description language >>> in which the tape alphabet is limited to {'0','1',' '}. No program's >>> source code can appear on the tape, because every XML document contains >>> '<' etc., yet the language is Turing-complete. >> >> But that's simply a matter of encoding, they're >> information-theoretically equivalent. Something that outputs >> 100100011010010100001 >> or >> 010010000110100100100001 >> or the baudot equivalent, or... >> has, in my opinion, output 'Hi!'. >> >> If you have turing machine that can only output blank and mark, then >> it can never output zero using your logic, yet I presume that turing >> machines which had such an alphabet were used for arithmetic examples >> in your Computability 101 course without you batting an eyelid. >> >> Phil > > The reproduce-your-own-source problem usually calls for the exact text > of the program source code, not just some encoding of it. > > It would be an easier problem if you were allowed to use an encoding. To > do it in e.g. Java I would pick the encoding in which: > > "public static void main(String[] args){System.out.print(1);}" Forgot the class wrapper: "public class PrintOne{public static void main(String[] args){System.out.print(1);}}" > is represented by the number 1, and any other string is represented by > its Unicode encoding, treated as an integer, plus 10. > > This is a very different sort of problem from the usual computability > problems. Solving the empty tape halting problem cannot be made easier > by any changes in how "halts" and "does not halt" are represented in the > output. As long as, of course, there are distinct encodings for the two results, so that the encoding preserves information. Patricia
From: Charlie-Boo on 13 Sep 2006 12:46 Peter_Smith wrote: > Charlie-Boo wrote: > > > How can you conclude that a given formal proof proves a particular > > published theorem if you don't draw a correspondence between what is > > proven and that published theorem (C)? > > Perhaps what is causing trouble here is that you are assuming that > *formal* = *uninterpreted*, so that a formal proof needs to be > supplemented with some intepretative gloss before, as you put it, we > get a correspondence between what is proven and that published theorem. > But formal doesn't mean uninterpreted: proving a theorem in a > formalized language is like proving it in Polish (only better! ;-). > > A Polish mathematician is still proving arithmetical claims, even if he > doesn't use the words "two" and "three". Likewise a formalized proof in > Gödel's P can also be proving the same arithmetical claims, even > though P doesn't the words "two" and "three" either. I agree. I am not saying that it can't correspond to the published proof. I am just saying that you have to show that correspondance. You have the purported formal proof, and you have the published article with its proof. Now, don't you have to do something to show that the former is in fact proving the latter? "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 C-B
From: Charlie-Boo on 13 Sep 2006 12:54 Peter_Smith wrote: > Charlie-Boo wrote: > > >Can anybody show a single example of a formal > > derivation of a result from any branch of Computer Science? For > > example: > > > 4. Incompleteness in Logic: A formal derivation of Godel's > > Incompleteness theorems > > Well, we know that once the Hilbert-Bernays derivability conditions are > in place, there are easy formal derivation of Con_T --> not-Prov(#G_T), > using # for "the Gödel number of ...). > > And starting with Hilbert-Bernays there are textbook outlines of formal > proofs that the derivability conditions hold for theories with Sigma_1 > induction. See e.g. Boolos's book. > > That looks like a formal derivation to me. What more do you want?? You are talking about people taking a single proof and specifying at each step exactly what they are doing. But that does not give us an algorithm for applying every possible rule at each step, or to continue until the theorem is proven. It also does not show that what they proved corresponds to any particular published theorem. If one has an algorithm for applying all possible rules until a theorem is proven, then you can run this algorithm to create theorems. You have formal (automated) theorem-proving. You are able to produce new theorems. Just run the algorithm and theorems are created. But nobody has done this for the theorems of Computer Science - Program Synthesis, Theory of Computation, Recursion Theory or Incompleteness in Logic. Even those who claim to have formalized a single specific theorem have never shown how multiple similar theorems (from the same branch of Computer Science) can be created from a single set of rules. There are a number of papers that purport to have formalized a single theorem. But none shows how multiple theorems can be created in the process. For example, if it creates Turing's unsolvability of the Halting Problem, why doesn't it also produce and show the self-halting problem, the ever-halting problem, the always-halting problem, or the membership problem unsolvable? Similarly for papers that claim to formalize Godel's 1st. Incompleteness Theorem (though in reality there are two versions.) Why does it not also produce both versions of Godel's 1st. Incompleteness Theorem or Rosser's improvement? The answer is that they have merely gone through one proof and declared that they have "formalized" each step. But they have not created a general method of creating those steps and combining them to form a theorem. It only produces what they manually describe. There is no algorithm or general theorem-proving method shown for the various theorems within that branch of Computer Science. CBL === CBL has a small number of axioms and rules of inference. In fact, the same rules of inference are used for multiple branches of Computer Science. And from that small, fixed set of axioms and rules, we produce an array of theorems and variations, including new variations apparently not discussed in publications. There are short, formal proofs for both versions of Godel's 1st. Incompleteness theorem, Rosser's improvement and numerous Smullyan variations. That's the difference: one hand-coded example versus lots of formal examples. C-B
From: Peter_Smith on 13 Sep 2006 13:05 C-B wrote > I agree. I am not saying that it can't correspond to the published > proof. I am just saying that you have to show that correspondance. > You have the purported formal proof, and you have the published article > with its proof. Now, don't you have to do something to show that the > former is in fact proving the latter? I hesitate to reply to something that starts "I agree" ;-)) Let me put the question back to you: does a Polish mathematician who settles some arithmetical conjecture have to do something in addition to writing out his proof in Polish? Surely, not as part of his proof. Given most of us don't speak Polish, he might have to help us out with a translation, of course: but that isn't part of his proof -- he's just having to accommodate himself to the fact that we can't understand his perfectly good proof. Likewise, the translation manual from PM or Gödel's P to ordinary English maths-speak isn't part of the proof in PM or P. So: we should distinguish what is part of the formal proof itself from commentary on the proof.
From: Alec McKenzie on 13 Sep 2006 13:39
"Charlie-Boo" <shymathguy(a)gmail.com> wrote: > Alec McKenzie wrote: > > "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > > What do you call a system that contains a representation for every > > > recursive function? > > > > I would not dream of trying to call it anything. Does it have > > some bearing on programs that output themselves? > > Yes. It is what is often called a "Base of Computing" or a > "Programming Language", and is the context in which we can show there > is a program that outputs itself. > > Actually, using CBL we can see the exact sufficient condition that a > Programming Language meets: Substitution is recursive. > > A. Let M # f(I) mean program M outputs the value of function f applied > to input I. > > B. Define function s11(I,J) as M # f(I) => s11(M,N) # f(N). (S11 > substitutes a constant J for the single input variable in program I.) > > C. Let f(I) mean f is recursive. Then the axiom is s11(I,J), > substitution is recursive. > > D. By definition, we have f(I) <=> (eM) M # f(I) > > Thm. N # N There is a program that outputs itself. > 1. s11(I,J) Axiom C - Substitution is recursive. > 2. s11(I,I) Subtitution, 1 > 3. M # s11(I,I) Rule D, 2 > 4. s11(M,M) # s11(M,M) Rule B, 3 > 5. N # N Substitution, 4 > qed > > And of course the real test of the validity of any formal system is its > ability (or inability) to generate lots of useful theorems, both known > and new. CBL can prove not just the existance of a self-outputting > program, but also the Fixed Point theorem, the Recursion theorem, and > more complex theorems involving multiple functions and conclusions - > i.e. Recursion Theory. For example, if f(I) and g(I) then there is an > M,N such that M # f(N) + N # g(M). I see you are back to the existence of "*a* self-outputting program", the proof of which is trivial (i.e. a single example will do it). Why you should need CBL to generate a "useful theorem" of that kind?. -- Alec McKenzie usenet@<surname>.me.uk |