I ran into a very interesting (and fairly readable) paper that demonstrates remarkable algorithms for (1) finding the maximum of a continuous function on the real interval [0, 1] and (2) integrating a continuous function over the interval [0, 1]. What is interesting about this is that these algorithms work with exact reals, which represent real numbers as lazy bit streams (so the algorithms take a finite number of steps to compute the first k bits of the answer). Underlying these algorithms is “Berger’s search operator” which computes in finite time whether a proposition is true for all real numbers in [0, 1]. By itself, that is already remarkable! This function is just 5 lines of code (see Figure 1).
https://www.research.ed.ac.uk/portal/files/12417914/download_2.pdf
The author writes “The integration algorithm performs abysmally on any interesting functions. The maximum algorithm performs a little better.”. I would assume the speed problem is due to the Berger search being hopelessly slow (as it has an exponential blow-up in complexity as more bits become relevant). I have found another paper that gives substantially faster search algorithms for this problem, but unlike the previous paper, is not at all readable (at least to me). An interesting remark from the conclusion of the second paper: “this work is a genuine application of topology to computation: theorems formulated in the language of computation, proofs developed in the language of topology.”.
http://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf
Follow RSS/Atom feed for updates.