Goedel & programming languages

Quote:

>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{*filter*} of Science.

{hpfcla,hplabs}!hpldola!patch |