Computing with continuous objects: a uniform co-inductive approach

摘要

uniform approach to computing with infinite objects like real numbers, tuples of these, compacts setsand uniformly continuous maps is presented. In the work of Berger, it was shown how to extract certifiedalgorithms working with the signed digit representation from constructive proofs. Berger and thepresent author generalised this approach to complete metric spaces and showed how to deal with compactsets. Here, we unify this work and lay the foundations for doing a similar thing for the much morecomprehensive class of compact Hausdorff spaces occurring in applications. The approach is of the samecomputational power as Weihrauch’s Type-Two Theory of Effectivity.