FOM: Re: nonconstructive existence proofs of algorithms

[Miguel A. Lerma]

Stephen G Simpson wrote:
 > 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.

That has the same flavor as the known result stating that every real
computable function f:[0,1] -> R such that f(0)f(1) < 0 has a
computable zero in (0,1).  For each such function f there is an
algorithm that computes a zero for f in (0,1), but in general we do
not have such algorithm, we only know that it exists.  Since there is
no single algorithm that works for every f, the proof must be
nonconstructive - say by deriving a contradiction from the assumption
that f has no computable zero in (0,1).

However, if by "yielding an algorithm" we mean that an specific
algorithm can be derived from the proof, certain cardinality arguments
come to my mind.  For instance the existence of irrational numbers can
be proven non constructively by noting that Q is countable and R is
uncountable.  But this argument allows us to design an algorithm to
compute an irrational number in the following way: effectively
enumerate the rational numbers r_1, r_2, r_3,..., then compute an
irrational number x in (0,1) by letting its n-th decimal digit be
equal 0 if the n-th decimal digit of r_n is different from 0, and 1
otherwise.  A modification of this argument can be used to compute a
transcendental rather than just irrational number, as shown by Robert
Gray in The Am. Math. Mo. 101 (1994) 819-832.  More generally Lebesge
showed in Bull. Soc. Math. France 45 (1917) 132-144 how to transform
metric theorems into constructive proofs - which can be used to design
algorithms.



Miguel A. Lerma 
Lecturer 
Department of Mathematics 
Northwestern University 
Evanston, IL 60208