Intermediate value theorem on computable reals

Wikipedia says that the intermediate value theorem “depends on (and is actually equivalent to) the completeness of the real numbers.” It then offers a simple counterexample to the analogous proposition on ℚ and a proof of the theorem in terms of the completeness property.

Does an analogous result hold for the computable reals (perhaps assuming that the function in question is computable)? If not, is there a nice counterexample?

-
Have you read en.wikipedia.org/wiki/… already? –  Qiaochu Yuan Dec 15 '09 at 16:48
I'm afraid I don't understand your question. The IVT says that if a continuous function has range (y1,y2) over some interval (x1,x2) then for any yc between y1 and y2, there is some xc between x1 and x2 such that the function at f(xc) = yc. I don't understand how this is meant to be extended to the computable reals... –  Gabriel Benamy Dec 15 '09 at 16:56
Qiaochu Yuan: Thanks for the link. I'm not interested in adopting intuitionist logic; an existence proof would satisfy me. –  Jason Orendorff Dec 15 '09 at 17:37
Gabriel Benamy: Like this-- "If a continuous computable function f maps the computable reals in the interval [x1, x2] to computable reals, with f(x1)=y1 and f(x2)=y2, then for any computable number yc between y1 and y2, there is some computable number xc between x1 and x2 such that the function at f(xc)=yc." (Continuity is defined the same for the computable reals as for the reals, in case that's the difficulty.) –  Jason Orendorff Dec 15 '09 at 17:45
I can see that there's an existential quantifier in the IVT, and if it is to be proven, then that has to come from somewhere. If you write out the proof for the reals, that quantifier clearly comes from invoking the least upper bound property. If it's obvious that one just can't get an existential quantifier on the computable reals, then that's the piece I'm missing (and, in that case, sorry for the dumb question!) –  Jason Orendorff Dec 15 '09 at 17:51

Let me assume that you are speaking about computable reals and functions in the sense of computable analysis, which is one of the most successful approaches to the topic. (One must be careful, since there are several incompatible notions of computability on the reals.)

In computable analysis, the computable real numbers are those that can be computed to within any desired precision by a finite, terminating algorithm (e.g. using Turing machines). One should imagine receiving rational approximations to the given real. In this subject, functions on the reals are said to be computable, if there is an algorithm that can compute, for any desired degree of accuracy, the value of the function, for any algorithm that produces approximations to the input with sufficient accuracy. That is, if we want to know f(x) to within epsilon, then the algorithm is allowed to ask for x to within any delta it cares to.

The Computable Intermediate Value Theorem would be the assertion that if f is a computable continuous function and f(a)< c<f(b) for computable reals a, b, c, then there is a computable real d with f(d)=c.

The book Computable analysis: an introduction by Klaus Weihrauch discusses exactly this question in Example 6.3.6.

The basic situation is as follows. The answer is Yes. If f happens to be increasing, then the usual bisection proof of existence turns out to be effective. For other f, however, one can use a trisection proof. Theorem 6.3.8 says that if f is computable and f(x)*f(z)<0, then f has a computable zero. This implies the Computable Intermediate Value theorem above.

In contrast, the same theorem also says that there is a non-negative computable continuous function f on [0,1], such that the sets of zeros of f has Lebesgue measure greater than 1/2, but f has no computable zero.

In summary, if the function crosses the line, you can compute a crossing point, but if it stays on one side, then you might not be able to compute a kissing point, even if it is kissing on a large measure set.

-
What a great answer. Thanks. –  Jason Orendorff Dec 17 '09 at 6:53
Vasco Brattka, the most prominent of Weihrauch's followers, commented <a href="cs.nyu.edu/pipermail/fom/2009-May/013776.html">; on the FOM list<a> that the constructive critique of the IVT may be interpreted classically as (the failure of) a <i>uniform</i> assignment of a zero, ie continuously wrt the function (or parameters that describe it). This is the only observation about the IVT that I have heard from that school since I presented my paper on the IVT at <a href="cca-net.de/cca2005/">their conference</a>. –  Paul Taylor Jan 1 '10 at 16:35

Thanks first to Andrej for drawing attention to my paper on the IVT, and indeed for his contributions to the work itself. This paper is the introduction to Abstract Stone Duality (my theory of computable general topology) for the general mathematician, but Sections 1 and 2 discuss the IVT in traditional language first. The following are hints at the ideas that you will find there and at the end of Section 14.

I think it's worth starting with a warning about the computable situation in ${\bf R}^2$, where it is customary to talk about fixed points instead of zeroes.
Gunter Baigger described a computable endofunction of the square. The classical Brouwer thereom says that it has a fixed point, but no such fixed point can be defined by a program. This is in contrast to the classical response to the constructive IVT, that either there is a computable zero, or the function hovers at zero over an interval. (I have not yet managed to incorporate Baigger's counterexample into my thinking.)

Returning to ${\bf R}^1$, we have a lamentable failure of classical and contructive mathematicians to engage in a meaningful debate. The former claim that the result in full generality is "obvious", and argue by quoting random fragments of what their opponents have said in order to make them look stupid. On the other hand, to say that "constructively, the intermediate value theorem fails" by showing that it implies excluded middle is equally unconstructive.

Even amongst mainstream mathematicians several arguments are conflated, so I would like to sort them out on the basis of the generality of the functions to which they apply.

On the cone hand we have the classical IVT, and the approximate construtive one that Neel mentions. These apply to any continuous function with $f(0) < 0 < f(1)$.

There are several other results that impose other pre-conditions:

• the exact constructive IVT, for non-hovering functions, described by Reid;

• using Newton's algorithm, for continuously differentiable functions such that $f(x)$ and $f'(x)$ are never simultaneously zero; and

• the Brouwer degree, with an analogous condition in higher dimensions.

These conditions are all weaker forms of saying that the function is an open map.

Any continuous function $f:X\to Y$ between compact Hausdorff spaces is proper: the inverse image $Z=f^{-1}(0)\subset X$ of $0\in Y$ is compact (albeit possibly empty).

If $f:X\to Y$ is also an open map then $Z$ is overt too. I'll come back to that word in a moment.

When $f$ is an open map between compact Hausdorff spaces and $Z$ is nonempty, there is a compact subspace $K\subset X$ and an open one $V\subset Y$ with $0\in V$ and $V\subset f(K)$.

So for real manifolds we might think of $K$ is a (filled-in) ball and $f(K)\setminus V$ as the non-zero values that $f$ takes on the enclosing sphere.

Could I have forgotten that the original question was about computability?

No, that's exactly what I'm getting at.

In ${\bf R}^1$ an enclosing sphere is a straddling interval, $[d,u]$ such that $f(d) < 0 < f(u)$ or $f(d) > 0 > f(u)$.

The interval-halving (or, I suspect, any computational) algorithm generates a convergent sequence of straddling intervals.

More abstractly, write $\lozenge U$ if the open subset $U$ contains a straddling interval. The interval-halving algorithm (known historically as the Bolzano--Weierstrass theorem or lion hunting) depends exactly on the property that $\lozenge$ takes unions to disjunctions, and in particular $$\lozenge(U\cup V) \Longrightarrow \lozenge U \lor \lozenge V.$$ (Compare this with the Brouwer degree, which takes disjoint unions to sums of integers.)

I claim, therefore, that the formulation of the constructive IVT should be the identification of suitable conditions (more than continuity but less than openness) on $f$ in order to prove the above property of $\lozenge$.

Alternatively, instead of restricting the function $f$, we could restrict the open subsets $U$ and $V$. This is what the argument at the end of Section 14 of my paper does. This gives a factorisation $f=g\cdot p$ of any continuous function $f:{\bf R}\to{\bf R}$ into a proper surjection $p$ with compact connected fibres and a non-hovering map $g$.

To a classical mathematician, $p$ is obviously surjective in the pointwise sense, whereas this is precisely the situation that a constructivist finds unacceptable. Meanwhile, they agree on finding zeroes of $g$.

In fact, this process finds interval-valued zeroes of any continuous function that takes opposite signs, which was the common sense answer to the question in the first place.

The operator $\lozenge$ defines an overt subspace, but I'll leave you to read the paper to find out what that means.

-

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.

-
Indeed, the Computable IVT as I stated it is equivalent to (a), and this is what Weirich proves (and what the questioner seems to have asked). A major goal of computable analysis is to undertand the computable reals as a mathematical structure, using classical logic, and it is statement (a) that implies, for example, that the computable reals are a real-closed field. (See Weirich Corollary 6.3.10.) Statement (b), in contrast, requires a uniform algorithm, which is a stronger notion. Such uniformity issues arise throughout compubility theory, both on the natural numbers and on the reals. –  Joel David Hamkins Dec 22 '09 at 1:48

This question and its answers confused me for a while, but I think I get it now, so I'll describe my experience in the hopes that it will help other non-experts, and the experts can tell me if I've still got anything wrong.

My initial reaction was: given a computable function f : [a, b] → ℝ with f(a) < 0 and f(b) > 0, "of course" we can compute an element z of [a, b] with f(z) = 0, as follows: choose c to be the midpoint (a+b)/2, check whether f(c) is positive or negative, report that z is in [a, c] or [c, b] respectively, and recurse on that interval. Ironically, the problem is that f(c) might actually be exactly 0. If so, we can ask for its value to arbitrarily large precision, but will never learn anything about whether it is positive, negative, or zero, so we cannot output c as the answer, nor guarantee that either subinterval [a, c] or [c, b] contains a root of f.

Under the locally non-constant hypothesis, however, we can choose c' near c (so that both intervals [a, c'] and [c', b] are less than k times as wide as [a, b] for some fixed k < 1) so that f(c) and f(c') are distinct. Then we can compute f(c) and f(c') in parallel, stopping when we know that one of them is either positive or negative, as must eventually happen since they cannot both be zero, and proceed as before.

It's also clear now why classically there is a computable root of f without any hypotheses besides computability of f: either some number of the form a + (s/2r)(b-a) is a root of f—these numbers are all computable—or the original algorithm will succeed forever and thus compute a root of f.

-
Tjhat is an accurate description of what is going on, yes. –  Andrej Bauer Dec 22 '09 at 16:36
Yes, I agree... –  Joel David Hamkins Dec 24 '09 at 20:36
This is the "interval-halving" proof of the "exact" constructive IVT for functions that "don't hover" or are "locally not constantly zero". –  Paul Taylor Jan 1 '10 at 19:18
$\forall n.\; \exists x \in [a,b].\; |f(x) − c| < 2^{−n}$