Suppose that is a continuous function from to and that we have a program which computes it. (Ignore for now exactly what it means to “compute” a real-valued function of the reals. Suffice it to say that almost every natural continuous function you come across is computable). If we want to compute , say to within an accuracy of , how would we do it, and would we need any further information about in order to do it?

The obvious thing to do is to compute a Riemann sum for some large . However, this could be arbitrarily far from the true value of . For example, might be 0 for all , but might curve sharply up in between each and so that its definite integral is arbitrarily close to 1.

However, since is continuous on , it is uniformly continuous. This means that for all there is a such that whenever , . If we could compute a function such for all , whenever , , then we could compute the definite integral of with arbitrary accuracy: If we want to know to within 0.001, then choose so that and we can take , since .

So, one answer to the question “What extra information do we need in order to compute ?” is: a function witnessing ‘s uniform continuity.

In 1998, Alex Simpson showed, building on ideas of Ulrich Berger and others, that another answer is: Nothing!

For technical convenience, we switch from considering functions with domain and range to functions with domain and range , and try to compute the definite integral of such a function over , since that value will again be in .

For our representation of the reals in we will use functions from to , where we are thinking of as representing . All reals in have representations. Some have more than one, but that won’t concern us.

We will use to denote both the interval of reals from to and the set of its representations. Hopefully this will not cause confusion.

So a computable function from to is a computable second-order functional which takes a function from to and returns a function from to . (There are some technicalities about the fact that a real can have more than one representation, but we will ignore them.)

Similarly, a predicate on is a function from to . An amazing fact due to Ulrich Berger is that for any computable predicate we can decide whether or not there is an such that holds. (To see why this is amazing, observe that the analogous statement for computable predicates on the integers is false, due to the Halting Problem.)

What’s more, we can define computable functionals and so that, if is a computable predicate, returns or depending on whether or not and returns a number which satisfies if anything does.

Before we define those functions, I’ll give some notation. If is a function from to , then we let be defined by and for . We define and similarly.

Now define and by mutual recursion as follows: Let and let do the following: it uses checks to see if there is an such that and holds and, if so, it returns , where . If not, it uses to check if there is an such that and holds and if so, it returns , where . If both of those fail, it returns , where .

If you think about the above definitions for a while, it should probably become clear to you that they should work, if they terminate. But they seem way too crazy to terminate. In fact they do, given one condition which I’ll remark on below, and the crucial fact is that since is computable and total, when given an , it only looks at finitely many values before terminating.

The condition that allows them to terminate is that we specify that the evaluation is lazy. That is, when I say for example that returns , I mean that it returns the function which on input returns and only on non-zero input calculates to determine its return value for that input. So, it only calls when it needs to. Since every call to involves a recursive call to , if you followed all of them immediately, the program could not possibly terminate.

Note also that we can use to define a as well.

Now let’s use this to compute the definite integral. Observe that if , then , if , then , and if , then . Conversely, every real in has a representation such that , and similarly for the other two cases.

Therefore, if is such that for all , it must be the case that , and if we are trying to compute a representative for , we may safely say that , and similarly for the other two cases. Furthermore, if for all . Then .

Next, observe that, for any , by stretching it out and splitting it up, we may find and such that , and the range of on is equal to the range of on and the range of on is equal to the range of on

Therefore, the following definition for (almost) works: Given , first use to check if for all . If so, return . If not, check if for all or if for all and do the analogous thing. Otherwise, return .

Since is continuous, the process of splitting it up will eventually terminate, as will the algorithm.

Actually this algorithm doesn’t quite work, as there are some a couple of details that I’ve omitted, but it is essentially correct. For more information, see Alex Simpson’s paper, and for more on Berger’s work, see Martin Escardó’s blog post, both of which include actual runnable code.