Goedel & programming languages 
Author Message
 Goedel & programming languages

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.

--------------

Disclaimers:
        2 + 2 = 3, for suitably small values of 2
        Bill and Dave may not always agree with me



Sun, 19 Jul 1992 23:54:13 GMT  
 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     |



Mon, 20 Jul 1992 16:18:20 GMT  
 Goedel & programming languages

Quote:

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

  Career search in progress: ECE faculty. Research oriented. Will send vitae.
===============================================================================



Wed, 22 Jul 1992 06:30:16 GMT  
 Goedel & programming languages

See Fred Hennie's book ``Intro to Computability'' for a good look at
how that statement should go.

--

Department of Computer Science,            (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906



Wed, 22 Jul 1992 05:11:19 GMT  
 
 [ 4 post ] 

 Relevant Pages 

1. Goedel Programming Language

2. Goedel language available

3. ?gggerman doc's around the GOEDEL-language?

4. LP (prolog, Goedel) as a first language

5. Goedel language available

6. Goedel & SICStus Prolog

7. Workshop on Programming in Goedel

8. Visual Programming Languages Survey (Usability & Scalability)

9. Multi - Language Programs (CFW4b & Legacy)

10. Functional programming languages & formal verification

11. numerical & statistical programming in functional languages

12. Object Oriented Languages & Programming

 

 
Powered by phpBB® Forum Software