FOM: nonconstructive existence proofs of algorithms
richman at fau.edu
Thu Aug 10 11:03:28 EDT 2000
Stephen G Simpson wrote:
> By other work of Robertson and Seymour, if we knew S_n explicitly, we
> could explicitly write down a PTIME algorithm for deciding whether a
> given finite graph is of genus greater than n.
> Thus we have a nonconstructive proof that for each n there exists a
> PTIME algorithm for deciding whether a given finite graph is of genus
> greater than n. We do not have the algorithms themselves.
This example reminds me of a variant of the kind of example I
suggested earlier. Suppose we are interested in the halting problem
for C programs. The "bounded halting problem" is solvable classically.
That is, there is a nonconstructive proof that, for each n, there is
an algorithm A_n that takes as input a C program of length at most n,
returns 1 if that program halts, and returns 0 if it doesn't (the
algorithm is a finite table lookup).
I'm not exactly sure what "knowing S_n explicitly" means in Steve's
example. I assume that it means you have some sort of explicitly
defined function of n. If we had such a thing for A_n, we could solve
the (unbounded) halting problem. So we have a nonconstructive proof
that for each n there exists such an algorithm A_n, but we do not have
the algorithms themselves, nor will we ever have them (explicitly).
More information about the FOM