Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: John Thingstad on 13 Sep 2006 08:34 On Wed, 13 Sep 2006 04:05:05 +0200, Charlie-Boo <shymathguy(a)gmail.com> wrote: > > george wrote: >> > Alec McKenzie wrote [wrongly]: >> > > 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 >> >> C-B asks, >> > Why? >> >> Because there are a lot of simple easy-to-define >> programming languages in which you OBVIOUSLY can't do it, >> that's why. SOME programming languages are LAME. >> But despite being right about that, > > How in the world can you define "programming language" then? > I think what he means the language has to be Turing complete. http://en.wikipedia.org/wiki/Turing_completeness In essence you have to be able to write a Turing machine in the language and you also have to be able to have a Turing machine render the same functionality as the language. In general with a bit of experience you can see this. I find it easier to work with lambda calculus than Turing machines. http://en.wikipedia.org/wiki/Lambda_calculus my-recursive functions are Turing complete and thus it is a optional way of proving it. I find it easier to see the things a Turing complete language needs. When languages fail to provide Turing completeness it is usually because they only support regular languages. In particular you need support for 'the pumping theorem' http://www.google.com/search?rls=en&q=the+pumping+theorem&sourceid=opera&ie=utf-8&oe=utf-8 A simple test is: Can you write code to generate all permutations of a sequence? -- Using Opera's revolutionary e-mail client: http://www.opera.com/mail/
From: Charlie-Boo on 13 Sep 2006 08:37 Peter_Smith wrote: > > You can start with A, A formal statement of the theorem or result. > > This is in not a cogent response. 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. > Hilbert and Bernays indeed showed that Th has a formal > proof inside P. Then can you give A-F for Th, Godel's 1st. theorem (any version)? C-B
From: Charlie-Boo on 13 Sep 2006 08:39 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? C-B > -- > Alec McKenzie > usenet@<surname>.me.uk
From: Charlie-Boo on 13 Sep 2006 08:52 John Thingstad wrote: > >> Because there are a lot of simple easy-to-define > >> programming languages in which you OBVIOUSLY can't do it, > >> that's why. SOME programming languages are LAME. > >> But despite being right about that, > > How in the world can you define "programming language" then? > I think what he means the language has to be Turing complete. But no, he claims that "lame" (less powerful) languages are included among "Programming Languages". So I wonder how he defines what constitutes a Programming Language, then. > -- > Using Opera's revolutionary e-mail client: http://www.opera.com/mail/ You misspelled Oprah. C-B
From: Peter_Smith on 13 Sep 2006 09:03
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. |