|
Generally, constructive proofs are quite complicated. This is hardly surprising, since they produce more (computational) information than their classical counterparts (if the latter have any). Consider, for example, the constructive proofs of Picard�s theorem in the following two classically equivalent forms.
PTp
Let � be a holomorphic function on the punctured disc D (0,1) := {z ∈ C : 0 < |z| < 1} that omits two complex values from its range. Then � has a pole of determinate order at 0.
PTs
Let � be a holomorphic function on D(0,1) that has an essential singularity at 0, and let ζ, ζ′ be two distinct complex numbers. Then either there exists z ∈ D(0,1) with � (z) = ζ or else there exists z ∈ D(0,1) with � (z) = ζ′
These two theorems, although classically equivalent, are totally different from a constructive point of view. In PTp we use the data comprising the function � and the two complex values omitted from its range, to construct an integer ν, show that the νth Laurent coefficient of � is 0, and to show that all Laurent coefficients with index less than ν are zero. In PTs our data consist of the holomorphic function � and the two distinct complex numbers ζ, ζ′, and the constructive proof embodies an algorithm converting those data to solution z of one of the equations � (z) = ζ, � (z) = ζ′; moreover, the proof shows which equation is actually solved.
Now, it is hardly surprising that the constructive proofs of both PTp and PTs are rather complicated. For one thing, they rely on delicate estimates involving winding numbers and requiring a number of preliminaries that the classical proof of Picard�s theorem does not require. In addition, those algorithms could actually be extracted from the proofs and implemented on a computer. So we pay more in terms of effort and complexity of proof, but we get more for our money as well.
The complexity of constructive proofs, other than those that use the Church�Markov�Turing thesis as an additional hypothesis (see [21]) is still largely untouched terrain. However, anecdotal evidence from Bas Spitters suggests that, perhaps contrary to one�s initial expectations, many of the proofs in Bishop�s book are remarkably efficient when implemented on a computer.
|
