[FOM] Computing roots of a polynomial (was: isomorphism as identity)

[Daniel Méhkeri]

I wrote:
> I guess we have stumbled on a neat example where classical recursion
> theory and constructive mathematics are at odds: a constructive
> mathematician would disagree that c is rational! (To say
> "either T halts or it doesn't" is of course not kosher.)
[...]
> So it would be correct, as is, to say that for rational coefficients
> the roots are computable, without worry about the representation
> concerns mentioned.

Vaughan Pratt replied:

> Yes.  My interpretation of "polynomials with rational coefficients"
> is that they are presented in some decidable representation, which
> I understand to be the usual meaning.  This interpretation is not
> possible for "polynomials with computable coefficients" with the
> usual notion of "computable real."  My answer to Karim was only for
> the second case he asked about, namely computable coefficients.

But isn't it still possible for computable coefficients, since  constructive witnesses of the antecedents "the computable real x_n is rational" would still contain the necessary info for the consequent. This might be why your answer and Andrej's were inconsistent.

I found it interesting because I recall examples of this sort being contrived, where the classical answer is a trivial one along the lines of: "if P, then f(x) = +1 is a computable function satisfying the requirement, if not-P, then f(x) = -1 is a computable function satisfying the requirement." So either way there exists a function "computing" the answer, even if we don't know which trivial algorithm gives the answer. 

This one seems to have come up naturally. 

Well, somewhat. Admittedly Andrej started the root computations thread to make a certain related point.

Regards,
Daniel


      À la recherche du cadeau idéal? Offrez Flickr!
http://www.flickr.com/gift/