I am afraid Joel has missed an important detail there, which is worth pointing out. Suppose $f$ is continuous and computable on $[a,b]$ and $f(a) \cdot f(b) < 0$. We must be careful to distinguish between

1. there exists a computable $x$ in $[a,b]$ such that $f(x) = 0$, and

2. there is an algorithm which accepts as input $f$, $a$, and $b$ and outputs $x$ in $[a,b]$ such that $f(x) = 0$.

In the first case we have a classical existence of a computable entity $x$, while in case (b) we have a computable existence of a computable entity.

I am pretty sure Weihrauch only proves 1., and it is impossible to prove 2., even if we further assume that $f$ is not only computable but computably continuous, or even Lipshitz with a known computable constant. The basic reason why 2. does not hold is that the $x$ cannot be chosen continuously with respect to the input data: essentially, a very small perturbation of $f$ can cause $x$ to jump around. Because all computable maps are continuos, we cannot have an algorithm computing $x$ (this is not a proof, just the idea, you have to work a bit harder to get all the details right).

However, you can impose fairly mild conditions on $f$ that are typically satisfied in practice. For example, if $f$ is locally non-constant, by which I mean that for every $y$ in $[a,b]$ we can compute nearby points $z$ and $w$ such that $f(z) \neq f(w)$, then IVT holds computably in the sense of 2. To see this, just perform bisection, but always avoid hitting a zero by going to a nearby non-zero point (because either $f(z)$ or $f(w)$ is non-zero, and we can compute which one). This condition is satisfied by non-trivial polynomials, for example, as well as for any differentiable function wose derivative only has isolated zeroes.

Let me also say a bit about the use of completeness of reals in IVT. Neel's remark translats from constructive mathematics to computability as follows: we can compute arbitrarily good approximations to the IVT. The trouble is that the approximations need not converge to anything, at least not computably. Classically they have an accumulation point, but we can't compute any information from it.

A second point is that IVT holds not because $\mathbb{R}$ is complete, but because it is connected. A very thorough analysis of this was made by Paul Taylor in his paper "A lambda-calculus for real analysis", see http://www.paultaylor.eu/ASD/lamcra/ . It's not easy reading, but it is very educational.

I am afraid Joel has missed an important detail there, which is worth pointing out. Suppose $f$ is continuous and computable on $[a,b]$ and $f(a) \cdot f(b) < 0$. We must be careful to distinguish between

1. there exists a computable $x$ in $[a,b]$ such that $f(x) = 0$, and

2. there is an algorithm which accepts as input $f$, $a$, and $b$ and outputs $x$ in $[a,b]$ such that $f(x) = 0$.

In the first case we have a classical existence of a computable entity $x$, while in case (b) we have a computable existence of a computable entity.

I am pretty sure Weihrauch only proves 1., and it is impossible to prove 2., even if we further assume that $f$ is not only computable but computably continuous, or even Lipshitz with a known computable constant. The basic reason why 2. does not hold is that the $x$ cannot be chosen continuously with respect to the input data: essentially, a very small perturbation of $f$ can cause $x$ to jump around. Because all computable maps are continuos, we cannot have an algorithm computing $x$ (this is not a proof, just the idea, you have to work a bit harder to get all the details right).

However, you can impose fairly mild conditions on $f$ that are typically satisfied in practice. For example, if $f$ is locally non-constant, by which I mean that for every $y$ in $[a,b]$ we can compute nearby points $z$ and $w$ such that $f(z) \neq f(w)$, then IVT holds computably in the sense of 2. To see this, just perform bisection, but always avoid hitting a zero by going to a nearby non-zero point (because either $f(z)$ or $f(w)$ is non-zero, and we can compute which one). This condition is satisfied by non-trivial polynomials, for example, as well as for any differentiable function wose derivative only has isolated zeroes.

Let me also say a bit about the use of completeness of reals in IVT. Neel's remark translates from constructive mathematics to computability as follows: we can compute arbitrarily good approximations to the IVT. The trouble is that the approximations need not converge to anything, at least not computably. Classically they have an accumulation point, but we can't compute any information from it.

A second point is that IVT holds not because $\mathbb{R}$ is complete, but because it is connected. A very thorough analysis of this was made by Paul Taylor in his paper "A lambda-calculus for real analysis", see http://www.paultaylor.eu/ASD/lamcra/ . It's not easy reading, but it is very educational.

I am afraid Joel has missed an important detail there, which is worth pointing out. Suppose f is continuous and computable on [a,b] and f(a)*f(b) < 0. We must be careful to distinguish between

(a) there exists a computable x in [a,b] such that f(x) = 0, and

(b) there is an algorithm which accepts as input f, a, and b and outputs x in [a,b] such that f(x) = 0.

In case (a) we have a classical existence of a computable entity x, while in case (b) we have a computable existence of a computable entity.

I am pretty sure Weihrauch only proves (a), and it is impossible to prove (b), even if we further assume that f is not only computable but computably continuous, or even Lipshitz with a known computable constant. The basic reason why (b) does not hold is that the x cannot be chosen continuously with respect to the input data: essentially, a very small perturbation of f can cause x to jump around. Because all computable maps are continuos, we cannot have an algorithm computing x (this is not a proof, just the idea, you have to work a bit harder to get all the details right).

However, you can impose fairly mild conditions on f that are typically satisfied in practice. For example, if f is locally non-constant, by which I mean that for every y in [a,b] we can compute nearby points z and w such that f(z) != f(w), then IVT holds computably in the sense of (b). To see this, just perform bisection, but always avoid hitting a zero by going to a nearby non-zero point (because either f(z) or f(w) is non-zero, and we can compute which one). This condition is satisfied by non-trivial polynomials, for example, as well as for any differentiable function wose derivative only has isolated zeroes.

Let me also say a bit about the use of completeness of reals in IVT. Neel's remark translats from constructive mathematics to computability as follows: we can compute arbitrarily good approximations to the IVT. The trouble is that the approximations need not converge to anything, at least not computably. Classically they have an accumulation point, but we can't compute any information from it.

A second point is that IVT holds not because R is complete, but because it is connected. A very thorough analysis of this was made by Paul Taylor in his paper "A lambda-calculus for real analysis", see http://www.paultaylor.eu/ASD/lamcra/ . It's not easy reading, but it is very educational.

I am afraid Joel has missed an important detail there, which is worth pointing out. Suppose $f$ is continuous and computable on $[a,b]$ and $f(a) \cdot f(b) < 0$. We must be careful to distinguish between

1. there exists a computable $x$ in $[a,b]$ such that $f(x) = 0$, and

2. there is an algorithm which accepts as input $f$, $a$, and $b$ and outputs $x$ in $[a,b]$ such that $f(x) = 0$.

In the first case we have a classical existence of a computable entity $x$, while in case (b) we have a computable existence of a computable entity.

I am pretty sure Weihrauch only proves 1., and it is impossible to prove 2., even if we further assume that $f$ is not only computable but computably continuous, or even Lipshitz with a known computable constant. The basic reason why 2. does not hold is that the $x$ cannot be chosen continuously with respect to the input data: essentially, a very small perturbation of $f$ can cause $x$ to jump around. Because all computable maps are continuos, we cannot have an algorithm computing $x$ (this is not a proof, just the idea, you have to work a bit harder to get all the details right).

However, you can impose fairly mild conditions on $f$ that are typically satisfied in practice. For example, if $f$ is locally non-constant, by which I mean that for every $y$ in $[a,b]$ we can compute nearby points $z$ and $w$ such that $f(z) \neq f(w)$, then IVT holds computably in the sense of 2. To see this, just perform bisection, but always avoid hitting a zero by going to a nearby non-zero point (because either $f(z)$ or $f(w)$ is non-zero, and we can compute which one). This condition is satisfied by non-trivial polynomials, for example, as well as for any differentiable function wose derivative only has isolated zeroes.

Let me also say a bit about the use of completeness of reals in IVT. Neel's remark translats from constructive mathematics to computability as follows: we can compute arbitrarily good approximations to the IVT. The trouble is that the approximations need not converge to anything, at least not computably. Classically they have an accumulation point, but we can't compute any information from it.

A second point is that IVT holds not because $\mathbb{R}$ is complete, but because it is connected. A very thorough analysis of this was made by Paul Taylor in his paper "A lambda-calculus for real analysis", see http://www.paultaylor.eu/ASD/lamcra/ . It's not easy reading, but it is very educational.