Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uwm.edu!zaphod.mps.ohio-state.edu!usc!ucsd!ucsdhub!hp-sdd!hplabs!hpfcso!hpldola!patch
From: patch@hpldola.HP.COM (Pat Chkoreff)
Newsgroups: comp.lang.misc
Subject: Re: Goedel & programming languages
Message-ID: <11470002@hpldola.HP.COM>
Date: 1 Feb 90 08:18:20 GMT
References: <8960009@hpfcso.HP.COM>
Organization: HP Elec. Design Div. -ColoSpgs
Lines: 68

/ 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     |