Experiments on an Internal Approach to Typed Algorithms in Analysis
The chapter consists of four sections. First we discuss aspects of generalized computability theory with a focus of how various approaches to abstract computability theory relate to computational analysis. Emphasis is put on the distinction between internal and external algorithms. Then we prove some old and some new results related to the typed hierarchy of hereditarily total objects over complete and separable normed vectorspaces, with the aim of carrying out the arguments within the framework of Kuratowski limit spaces.
In the final section we prove a topological consequence of an assumption that the total continuous functions from one complete, separable metric space to another is dense in the sense of domain theory. It turns out that this assumption will have consequences for how the connectedness properties of the two metric spaces relate.