On formally undecidable programs (was: Re: volatile: a summary)

[Steven Ryan]

(My chagrin at not realising this earlier is offset only by nobody else
realising it either.)

A perfect compiler is impossible.

The argument is quite simple and does not assert or deny the Church-Turing
(CT) hypothesis.

An optimiser transforms an input string into an output string such that certain
properties of the input string are retained (possibly translated) in the
output string. In other words, the optimiser is a theorem prover. And because
it is embedded in a formal system (a computer, remember, which is equivalent
to a turing machine), its ability to decide propositions about the string
(to determine and maintain valid properties) is limited by Godel's theorem.

Therefore, there exists strings whose properties are either undecidable
(in which case the optimiser is incomplete and imperfect) or inconsistently
decided (in which case the optimiser produces bad code and is imperfect).

How could such a program be written? It is not necessary to transcend CT but
just sidestep it: hire a staff of monkey programmers (they work cheap--you
can pay them peanuts) and let them bang away. They will produce correct
programs, once in awhile, once in a greate while, which defy reason. These
would unreasonble programs in the sense that they are random and no reasonable
reasoning could find a reason why they are correct. Such unreasonable,
undecidable programs must exist or the compiler is inconsistent.

Why not let the same staff bang out a perfect compiler then? Because Godel's
theorem does not make any restriction on how the steps of a theorem are
chosen, it is perfectly acceptable to consult an oracle, but that within a
formal system, it is impossible to construct the theorem. Any compiler which
is complete and consistent (thus perfect) and transcends Godel transcends
the CT hypothesis. Yet the existence of a perfect compiler was asserted by
implicit assuming CT, when it was stated that a perfect compiler can
understand anything a human can understand. I do not invoke CT--it is the
perfect compiler that both asserts and denies CT. Again the choice between
incompleteness or inconsistency.

Of course, a lot depends on the definition of a "perfect" compiler. I am
assuming a perfect compiler is consistent and can handle all possible
correct programs. "Perfect" is a rather transcendal word and to restrict it
to reasonable programs (programs a formal system can reason about), tarnishes
the word.

If you are still reading reading this and have read my previous notice, I
think you understand why I object to blithely asserting the existence of
algorithms without arguing from a solid foundation. While forming my thoughts
for this note, I now understand the flaw in Chris Torek's original
assertion of a perfect compiler: it was assumed it would only have to deal
with reasonable programs.

How good is this assumption? If it is possible to separate reasonable and
unreasonable programs, it might be acceptable. How would they separated?
If CT is assumed, the only decision procedure is a partial recursive predicate
which means we could identify reasonable programs but cannot guarentee
identification of unreasonable programs in finite time. If CT is denied,
separation in finite time might be possible, but that transcends the power
of whatever computer the compiler is running on.

If you want a real mess, consider programs that are syntactically correct and
do not fault at runtime but are still incorrect. 

Why is necessary to identify unreasonable programs? We're all reasonable
people, right? Right. Try maintaining code. Also, anybody whose says they
only have to deal with reasonable programs has never had to have a compiler
passed by a test and evaluation group.

Oh, right, this discussion is about volatile and C. Well, the point I've
been trying to make all along is that there is no such thing as free lunch.
It's a tradeoff between how much effort you exert in explaining your code
and how much effort somebody else exerts in understanding it. After all,
haven't our teachers and wise men been telling us for years to document our
code and explicitly state our invariants and assertions and other formal
properties? (Don't expect programmers who write optimisers to be any less
lazy than you.)

Now, be quiet. I have to write a letter to my (?)elected representatives.
Talk about unreasonble.

                                          sm ryan

               Religion isn't knowing the answers,
               it's knowing there are answers.
                              -- Marcia Rand