On Wed, Apr 13, 2005 at 11:01:11AM -0400, der Mouse wrote:
>
> Take the code for the checker. Wrap it in a small amount of code that
> makes a deliberate out-of-bounds access if the checker outputs `no
> problem'. Then write another small bit of code which ignores its input
> and runs the wrapped checker on itself.
>
> Run the original checker on the result.
>
> This is basically the same diagonalization argument Turing used to
> demonstrate that the Halting Problem was unsolvable; that's the sense
> in which I call it the Halting Theorem rephrased.
First off, I think you're more or less correct. Sortof. There is no
computable predicate that will decide for any ARBITRARY PROGRAM whether
ANY ARBITRARY CONSTRAINT is satisfied. But, this is just the statement
of the fact that there are constraints that are, themselves, not
computable.
But, this is highly naive. A useful checker would not be designed to try
to meet this objective. I think that's why he used the term "constrained
environment."
So, there are lots of cool ways to constraint the environment. You
could constrain the language in order to make certain constraints easy
to prove. You would still be unable to make proofs about all constraints,
but the sub-theory you're working in for a particular constraint might
be complete, which means that whether a program meets that constraint
would be fully computable.
This is just the assertion that if T is a deductively closed theory (in
logic) and S is a sub-theory, that T's incompleteness doesn't imply S's
incompleteness. At one level, this is just the statement that every
formal theory contains Logic itself as a sub-theory and that logic is
complete (Goedel's Completeness Theorem). Another more interesting
example is the sub-theory of Number Theory that contains only zero, the
successor function, and addition. Its a perfectly good sub-theory of
Number Theory and its been proved complete. But, its embedded** within a
much stronger Number Theory that's not complete.****
Also, one might seek to constrain the program's resource use during a
given computation. E.g., build the run-time environment with a suitably
strict watch-dog. Then, infinite loops may be made impossible and every
constraint becomes fully computable. This is basically computation
within the realm of strictly recursive functions, rather than the larger
class of partial recursive functions. So, you may be in trouble if the
program you need to write is a partial recursive function.
There's some interesting semantics of programming language being built
on top of Topological Fixed Point Theory. I read about it briefly, but
can't really comment on how well it addresses this problem. It seems to
be a promising possibility, though. See Nielson for more.
ciao,
-nash
"Semantics with Applications", Nielson & Nielson, Wiley, 1992. Available
as a PDF here: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html
** By "embedded" I mean in the strict mathematical sense, but in this
case the formal languages do not differ, so we can be a bit loose.
It is not necessary that this happen, though. The Arithmetization
technique used by Goedel gives us nice ways of embedding theories
from other languages into a larger theory. Also, I think this is more
or less what Cohen does with Forcing languages.
**** In fact, all of mathematics is considered (by logicians) to be
embedded inside what's called Set Theory (typically given by an
axiom system called ZFC). Set Theory is very powerful and is hence,
incomplete. But, there are lots of theories in mathematics that are
complete. The Theory of the Real Field, the above Number Theory, and
others. Here are some references:
http://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory
http://www.solace.net/nash/math/Set_Theory/zfc_axioms.pdf
"The Handbook of Mathematical Logic", Jon Barwise, North Holland
Publishing Co., 1977. ISBN 0 444 86388 5. (No longer in print, but
you may find a copy at your local Univ. library)
>
> > I really do find this line of argument rather irritating; the
> > theoretical limits of proof are quite a different thing from the
> > practical application of proof-based technology in a suitably
> > constrained environment.
>
> Entirely true. But if you use theoretical language like "proof", you
> have to expect to be held to a theroetical standard of correctness.
>
> /~\ The ASCII der Mouse
> \ / Ribbon Campaign
> X Against HTML [EMAIL PROTECTED]
> / \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B
--
An ideal world is left as an exercise for the reader.
- Paul Graham
