mjs@hpfcso.HP.COM (Marc Sabatella) (01/31/90)
An off the wall question: Everyone knows the basic diagonalization argument showing that there are some number-theoretic functions which are not computable. But after reading Hofstadter's pop-philosophy classic, "Goedel, Escher, Bach", in which the author makes several (rather lame) analogies from Goedel's Incompeteness theorem to, among other things, DNA and record players, I wonder if there is not a more powerful statement to be made. To wit, taking "formal system" to be programming language, and "proof" to be the parse tree and other semantic gizmos which purport that a program is valid in a particular language (in essence, a compilation), then what do you think of the following statement: For any programming language which is "sufficiently powerful" (meaning powerful enough to write a compiler for itself?), and any compiler for that language, there exists a valid program in the language which cannot be compiled. -------------- Marc Sabatella (marc%hpfcrt@hplabs.hp.com) Disclaimers: 2 + 2 = 3, for suitably small values of 2 Bill and Dave may not always agree with me
patch@hpldola.HP.COM (Pat Chkoreff) (02/01/90)
/ hpldola:comp.lang.misc / mjs@hpfcso.HP.COM (Marc Sabatella) / 8:54 am Jan 31, 1990 / >An off the wall question: > >Everyone knows the basic diagonalization argument showing that there are some >number-theoretic functions which are not computable. But after reading >Hofstadter's pop-philosophy classic, "Goedel, Escher, Bach", in which the >author makes several (rather lame) analogies from Goedel's Incompeteness >theorem to, among other things, DNA and record players, I wonder if there is >not a more powerful statement to be made. > >To wit, taking "formal system" to be programming language, and "proof" to be >the parse tree and other semantic gizmos which purport that a program is valid >in a particular language (in essence, a compilation), then what do you think of >the following statement: > > For any programming language which is "sufficiently powerful" (meaning > powerful enough to write a compiler for itself?), and any compiler for > that language, there exists a valid program in the language which > cannot be compiled. Here we say that a "compiler" is some effective procedure which decides whether or not a program is a valid member of the language. Then certainly there are languages which do not have compilers, e.g., the set of all tapes for which a Turing machine halts. But you're talking about languages which do have compilers. In our terminology, if a language has a compiler, then a program is valid if and only if it can be compiled. If that's true, then your statement is simply false: there can't be a valid program which cannot be compiled. But that isn't what you mean, right? Allow me to summarize Godel's Incompleteness Theorem, so that I might see a way to sustain or disdain your analogy. In Godel's Incompleteness Theorem, we have a proposition G that is a statement within natural arithmetic. Since G is an arithmetic proposition, we hope to use the axioms of natural arithmetic to decide whether G is true or false. However, G is a cleverly encoded proposition which simply states that there is no proof of G using the axioms of natural arithmetic. It turns out that IF the axioms of natural arithmetic are consistent, then neither G nor its negation ~G can be proved using those axioms, i.e., G is undecidable. The proof has two parts. 1. Assume that there is a proof P of G. Thus, P is a proof that there is no proof of G. Since there is no proof of G, then P in particular is not a proof of G. Since we can infer within arithmetic that P both is and is not a proof of G, it follows that arithmetic is inconsistent. 2. Assume that there is a proof P of ~G. Thus, P is a proof that it is not the case that there is no proof of G. In short, P is a proof that there is a proof of G. Hence, there are proofs for both ~G and G. Since both a statement and its negation can be proved within arithmetic, it follows that arithmetic is inconsistent. The difficulty in sustaining an analogy with Godel's Incompleteness Theorem lies in coming up with an "undecidable" program, that is, a program G which can neither be accepted nor rejected by a compiler M for a language L. That is, M cannot decide whether G is a member of L or not. But we've already said that M is an effective procedure, so no such G can exist. I don't think that you'll be able to formulate a subtle "Godelian Bomb" for good old recursive sets. Are you trying to cause trouble, or what? (:-) Regards, Patrick Chkoreff 719-590-5983 | Trouble is the Enema of Science. {hpfcla,hplabs}!hpldola!patch |
steve@hubcap.clemson.edu ("Steve" Stevenson) (02/03/90)
See Fred Hennie's book ``Intro to Computability'' for a good look at how that statement should go. -- Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
cline@cheetah.ece.clarkson.edu (Marshall Cline) (02/03/90)
In article <8960009@hpfcso.HP.COM> mjs@hpfcso.HP.COM (Marc Sabatella) writes: >To wit, taking "formal system" to be programming language, and "proof" to be >the parse tree and other semantic gizmos which purport that a program is valid >in a particular language (in essence a compilation), then what do you think of >the following statement: > For any programming language which is "sufficiently powerful" (meaning > powerful enough to write a compiler for itself?), and any compiler for > that language, there exists a valid program in the language which > cannot be compiled. >Marc Sabatella (marc%hpfcrt@hplabs.hp.com) Marc's statement proposed application of Godel's Incompleteness is incorrect. The key to Godel's Incompleteness is not that a program can't be detected to be syntactically incorrect, but rather that NO MACHINE CAN (in general) DECIDE ANYTHING ABOUT WHAT A PROGRAM *DOES*. It is apparent that compilers exist, and that they CAN BE both correct and complete. But all they can (in general) detect is syntactic correctness of the program; they can (in general) have *no* complete knowledge about what a program *does*. Example: in the comp.lang.c flame war a year ago regarding the need for "volatile" in ANSI-C, some thought a compiler could detect if a program used a var in a "volitale" way. But this is (again, in general) impossible. Back to what you *can't* do: if you claim to have written a program in *any* language that detects *anything* about what another program *does*, you'll be incorrect -- there will always exist programs which your program will fail on. (naturally, if the target language is simplistic enough that it can't do arithmetic, you *can* succeed, but most of us wouldn't call that a "language"). Marshall Cline -- =============================================================================== Marshall Cline/ECE Department/Clarkson University/Potsdam NY 13676/315-268-3868 cline@sun.soe.clarkson.edu, bitnet: BH0W@CLUTX, uunet!clutx.clarkson.edu!bh0w Career search in progress: ECE faculty. Research oriented. Will send vitae. ===============================================================================