FOM: nonconstructive existence proofs of algorithms

[Fred Richman]

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).

--Fred