I had thought that to create, constructively, a continuous function, g, on ℝ from two continuous pieces, f1 and f2, requires that the two pieces have a non trivial overlap, say [a, b]. This overlap always you to decide for a given input x whether a < x or x < b. Depending on the outcome of this decision return either f1(x) or f2(x). Of course for the resulting function to be well defined requires that f1 and f2 agree on [a, b].
However at the small TYPES workshop Dr. Martín Escardó showed that one can create a continuous function from two pieces that only overlap at one point, a. Although this fact is perhaps well-known, it wasn’t known to me. To compute g(x) within ε, compute both f1(x) and f2(x) within ε∕2. If these two approximations are within ε of each other, then just return the average of the two approximations. Otherwise decide if x < a or a < x and return the appropriate approximation. To constructively do this requires the lemma f1(x) # f2(x) ⇒ x # a; however I think this can be proven from f1(a) = f2(a) if f1 and f2 are both uniformly continuous.
Although this is nice, in practice I just define g over ℚ and then lift it to a function over ℝ.
Dr. Escardó also showed that I can compute definite integrals with my Few Digits library because I keep the modulus of continuity around. It will be fun to implement it.
One interesting thing I’ve noticed is that one can still Riemann integrate a uniformly continuous function on ℚ ⇒ ℝ and still get the correct value. In fact the function doesn’t seem to need to be continuous. It looks to me like Riemann integrable functions ought to be defined over ℚ rather than over ℝ.