The unreasonable effectiveness of Nonstandard Analysis

The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. In particular, we provide an algorithm which takes as input the proof of a mathematical theorem from `pure' Nonstandard Analysis, i.e. formulated solely with the nonstandard definitions (of continuity, integration, differentiability, convergence, compactness, et cetera), and outputs a proof of the associated effective version of the theorem. Intuitively speaking, the effective version of a mathematical theorem is obtained by replacing all its existential quantifiers by functionals computing (in a specific technical sense) the objects claimed to exist. Our algorithm often produces theorems of Errett Bishop's Constructive Analysis. We shall work in Nelson's syntactic approach to Nonstandard Analysis, called internal set theory, and treat theorems up to the Stone-Weierstrass theorem. Notable results are that applying our algorithm to theorems involving nonstandard compactness, we rediscover, depending on the formulation of the latter, either totally boundedness, the preferred notion of compactness in constructive and computable analysis, or equivalences from the foundational program Reverse Mathematics. Finally, we establish that a theorem of Nonstandard Analysis has the same computational content as its `highly constructive' Herbrandisation. Thus, we establish an `algorithmic two-way street' between so-called hard and soft analysis, i.e.\ between the worlds of numerical and qualitative mathematics.