Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 13 Sep 2006 09:38 Peter_Smith wrote: > Charlie-Boo wrote: > > > Do you agree that a formal proof of a theorem would include the > > following? > > > > 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. > > No. Of course not. By "formal proof" I mean formal proof, as defined in > any standard logic textbook. A "formal proof" is D above, a way to create the theorems (an r.e. set.) But we are talking about more than that. We are talking about showing that such a formal proof corresponds to an existing published proof. "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 What is Einstein talking about? ("Nature" = the published proof.) How can you have a formal proof without a formal statement of the theorem (A)? The proof has to produce a statement that the theorem is true (proven.) If the process is formal, how could the representation of the theorem not be formal? 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)? C-B
From: Alec McKenzie on 13 Sep 2006 09:51 "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > Alec McKenzie wrote: > > "Charlie-Boo" <shymathguy(a)gmail.com> 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? > > > > A single counter-example is sufficient: consider a programming > > language for writing screen-savers to display pretty moving > > pictures of coloured patterns, and these moving patterns are the > > only output that a program written in that language is able to > > produce. > > > > Since the program itself is not a moving coloured pattern, it > > follows that no program in that programming language can output > > itself. So not "every programming language...". > > 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? -- Alec McKenzie usenet@<surname>.me.uk
From: Peter_Smith on 13 Sep 2006 09:51 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.
From: Patricia Shanahan on 13 Sep 2006 09:57 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);}" 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. Patricia
From: Charlie-Boo on 13 Sep 2006 10:11
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). C-B > -- > Alec McKenzie > usenet@<surname>.me.uk |