Experiments on an internal approach to typed algorithms in analysis (Q2906569)

This is a paper concerned with aspects of generalized computability theory and their relation to an internal approach to computational analysis. It combines a very useful discussion on the history and the motivation for generalizing computability theory with a deep mathematical study of spaces of functionals of higher finite type over separable real Banach spaces within the framework of limit spaces and with a proof of a topological consequence of the assumption that the total objects in the domain \(D_{X} \rightarrow D_{Y}\), where \(D_{X}, D_{Y}\) are the domain representations of the Polish spaces \(X\), \(Y\), respectively, are dense.NEWLINENEWLINEThe author has introduced the distinction between internal and external computability over a mathematical structure already in [Stud. Logic Found. Math. 109, 137--144 (1982; Zbl 0574.03035)] and has initiated what can be called a ``program of internal computability'' in his papers [Lect. Notes Comput. Sci. 5028, 467--475 (2008; Zbl 1142.03358); Log. Methods Comput. Sci. 5, No. 3, Paper No. 11, 21 p. (2009; Zbl 1215.03057); ibid. 7, No. 2, Paper No. 11, 20 p. (2011; Zbl 1232.03030); ``The continuous functionals as limit spaces'', in: U. Berger (ed.) et al., Logic, construction, computation. Frankfurt am Main: Ontos Verlag. Ontos Mathematical Logic 3, 353--379 (2012)] and in the present paper, which consists of four sections.NEWLINENEWLINEIn the first section the author surveys some directions of generalized computability theory relevant to current research and explains his central distinction between internal and external concepts of computability over a mathematical structure. As he mentions, ``the internal concepts must grow out of the structure at hand, while external concepts may be inherited from computability over superstructures via, for example, enumerations, domain representations, or in other ways.''NEWLINENEWLINEIn the second section the author focuses on computational analysis, which is ``classical computability theory extended to structures appearing in analysis.'' He explains why Weihrauch's TTE-approach to computational analysis is a very external one, and why domain representations over effective domains as a foundation for computational analysis can be ``as external as the TTE-approach'', although a carefully chosen domain can lead to more internal concepts than the TTE-approach. The author motivates his program as follows: ``our main reason is analogue to the reason why logicians should try to prove theorems in weak systems, the weaker tools we use to obtain a result, the more extra knowledge can be obtained from the process of obtaining the result.'' Finally, based on Grilliot theory of functionals of higher type, the author gives an example of a limit process within a normed vector space that can be considered internally computable.NEWLINENEWLINEIn the third section the author proves a combined embedding and density theorem for hierarchies of limit spaces where the base types are separable real Banach spaces. For that, he introduces the concepts of probabilistic projection and probabilistic selection. First he defines a probabilistic projection from a sequential space \(Y\) to a subset \(X\) of it, which includes a given family of finite subsets, and proves constructively its existence in case \(Y\) is a complete separable metric space. A sequential separable Hausdorff space admits a probabilistic selection if there is a probabilistic projection from the space to itself. Then the author extends his notions and existence results to the case of two sequential separable Hausdorff spaces, one of which is topologically embedded into the other. The core of the author's non-trivial proof is the induction step of his main theorem, and specifically the construction -- assuming two such spaces \(X\) and \(Y\), a given probabilistic projection with respect to the given topological embedding, and two separable real Banach spaces \(U\), \(V\) such that \(U\) is a closed subspace of \(V\) -- of a topological embedding of \(X \rightarrow U\) into \(Y \rightarrow V\) together with a corresponding probabilistic projection.NEWLINENEWLINE In the fourth section, the author proves, using the domain representation of metric spaces as constructed in the work of \textit{J. Blanck} [Ann. Pure Appl. Logic 83, No. 3, 225--247 (1997; Zbl 0867.03014)], that if \(X\), \(Y\) are separable, complete metric spaces with domain representations \(D_{X}\), \(D_{Y}\), respectively, such that the total objects in the domain \(D_{X} \rightarrow D_{Y}\) are dense in it (a total object in \(D_{X} \rightarrow D_{Y}\) maps total ideals to total ideals), then \(Y\) is compactly saturated over \(X\). This property of \(Y\) and \(X\), defined by the author in his aforementioned 2008 paper, where a proof of this result is only sketched, has as a consequence that any local property of connectedness in \(X\) implies a corresponding global one in \(Y\). This strong implication of the above supposed density theorem shows, according to the author, that ``the internal approach to density \(\dots\) may be as useful as using external approaches.'' Although the author recognises that the current development of his internal approach to computability in analysis does not provide yet ``easy-to-use, high-level, programming languages for computing in analysis'', his program of internal computability is mathematically and conceptually fruitful, as the extensions and the generalisations of the author's results in his related cited work show.NEWLINENEWLINEFor the entire collection see [Zbl 1235.03005].