Anthony Jackson wrote:
Onno Meyer wrote:
Travis replied to me:
I see no reason that the proof is only for machines, it also applies
to methods or procedures that involve one or more people.
If those people follow an algorithm. Humans can decide not to
do that.
If you're going to provide proof, you necessarily use an algorithm. Note
that certain types of unsolvable problems are only unsolvable from
within the system being analyzed, which means an _external_ computer may
be able to determine whether a given program will halt when the computer
that the program will run on cannot. This exception also applies to a
human analyzing a computer program -- because he's external, he can
solve problems that the computer cannot solve for itself.
Also many halting problems can be "solved" by finding a weak point and
changing the problem. That may sound like cheating, but it is still
very useful.
For example, software code verifiers trying to prove if a piece of code
"halts" or not cannot do it for arbitrary input. But it can suggest to
the programmer, "Hey, put a contract/assert here to limit the range of
inputs and then I can prove it."
for(i=0; i<x; i++) { print i } for unknown x may never halt, but:
assert(x >= 0 && x < 1000)
for(i=0; i<x; i++) { print i } will provably halt at 1000 or sooner.
There are similar fixes for other classes of problems where the fixes
are not necessarily pretty or elegant but result in answers that work
well enough in the real world.
--
Zan Lynx
[email protected]
"Knowledge is Power. Power Corrupts. Study Hard. Be Evil."
_______________________________________________
GurpsNet-L mailing list <[email protected]>
http://mail.sjgames.com/mailman/listinfo/gurpsnet-l
