We study the power of BSS-machines enhanced with abilities such as computing the measure of a BSS-decidable set or computing limits of BSS-computable converging sequences. Our variations coalesce into just two equivalence classes, each of which also can be described as a lower cone in the Weihrauch degrees. We then classify computational tasks such as computing the measure of Δ⁰₂-set of reals, integrating piece-wise continuous functions and recovering a continuous function from an L₁([0, 1])-description. All these share the Weihrauch degree lim.

We use ideas from computable analysis to formalize exact real number computation in the Coq proof assistant. Our formalization is built on top of the Incone library, a Coq library for computable analysis. We use the theoretical framework that computable analysis provides to systematically generate target specifications for real number algorithms. First we give very simple algorithms that fulfill these specifications based on rational approximations. To provide more efficient algorithms, we develop alternate representations that utilize an existing formalization of floating-point algorithms and interval arithmetic in combination with methods used by software packages for exact real arithmetic that focus on execution speed. We also define a general framework to define real number algorithms independently of their concrete encoding and to prove them correct. Algorithms verified in our framework can be extracted to Haskell programs for efficient computation. The performance of the extracted code is comparable to programs produced using non-verified software packages. This is without the need to optimize the extracted code by hand. As an example, we formalize an algorithm for the square root function based on the Heron method. The algorithm is parametric in the implementation of the real number datatype, not referring to any details of its implementation. Thus the same verified algorithm can be used with different real number representations. Since Boolean valued comparisons of real numbers are not decidable, our algorithms use basic operations that take values in the Kleeneans and Sierpinski space. We develop some of the theory of these spaces. To capture the semantics of non-sequential operations, such as the "parallel or", we use multivalued functions.

We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that it is possible to translate back and forth between such machines and names in the standard function encoding used in computable analysis. Put differently, among the operators on Baire space, exactly the partial continuous ones are implementable by continuous machines and the data that such a machine provides is a description of the operator as a sequentially realizable functional. Continuous machines are naturally formulated in type theories and we have formalized our findings in Coq as part of Incone, a Coq library for computable analysis. The correctness proofs use a classical meta-theory with countable choice. Along the way we formally prove some known results such as the existence of a self-modulating modulus of continuity for partial continuous operators on Baire space. To illustrate their versatility we use continuous machines to specify some algorithms that operate on objects that cannot be fully described by finite means, such as real numbers and functions. We present particularly simple algorithms for finding the multiplicative inverse of a real number and for composition of partial continuous operators on Baire space. Some of the simplicity is achieved by utilizing the fact that continuous machines are compatible with multivalued semantics.

We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the results of this paper extend the library. While full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The paper includes a brief description of the most important concepts of Incone and its sub libraries mf and Metric. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that the countably infinite product of a space with itself is isomorphic to a space of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also describe many non-computational results that support the correctness of definitions from the library. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers.

This paper provides an alternate characterization of second-order polynomial-time computability, with the goal of making second-order complexity theory more approachable. We rely on the usual oracle machines to model programs with subroutine calls. In contrast to previous results, the use of higher-order objects as running times is avoided, either explicitly or implicitly. Instead, regular polynomials are used. This is achieved by refining the notion of oracle-poly-time computability introduced by Cook. We impose a further restriction on oracle interactions to force feasibility. Both the restriction and its purpose are very simple: it is well-known that Cook's model allows polynomial depth iteration of functional inputs with no restrictions on size, and thus does not preserve poly-time computability. To mend this we restrict the number of lookahead revisions, that is the number of times a query whose size exceeds that of any previous query may be asked. We prove that this leads to a class of feasible functionals and that all feasible problems can be solved within this class if one is allowed to separate a task into efficiently solvable subtasks. Formally, the closure of our class under lambda-abstraction and application are the basic feasible functionals. We also revisit the very similar class of strongly poly-time computable operators previously introduced by Kawamura and Steinberg. We prove it to be strictly included in our class and, somewhat surprisingly, to have the same closure property. This is due to the nature of the limited recursion operator: it is not strongly poly-time but decomposes into two such operations and lies in our class.

This paper compares different representations (in the sense of computable analysis) of a number of function spaces that are of interest in analysis. In particular subspace representations inherited from a larger function space are compared to more natural representations for these spaces. The formal framework for the comparisons is provided by Weihrauch reducibility. The centrepiece of the paper considers several representations of the analytic functions on the unit disk and their mutual translations. All translations that are not already computable are shown to be Weihrauch equivalent to closed choice on the natural numbers. Subsequently some similar considerations are carried out for representations of polynomials. In this case in addition to closed choice the Weihrauch degree LPO∗ shows up as the difficulty of finding the degree or the zeros. As a final example, the smooth functions are contrasted with functions with bounded support and Schwartz functions. Here closed choice on the natural numbers and the lim $\lim $ degree appear.

We extend Kawamura and Cook's framework for computational complexity for operators in analysis. This model is based on second-order complexity theory for functionals on the Baire space, which is lifted to metric spaces via representations. Time is measured in the length of the input encodings and the output precision. We propose the notions of complete and regular representations. Completeness is proven to ensure that any computable function has a time bound. Regularity relaxes Kawamura and Cook's notion of a second-order representation, while still guaranteeing fast computability of the length of encodings. We apply these notions to investigate relationships between metric properties of a space and existence of representations that render the metric bounded-time computable. We show that time bounds for the metric can straightforwardly be translated into size bounds of compact subsets of the space. Conversely, for compact spaces and for Banach spaces we construct admissible complete regular representations admitting fast computation of the metric and short encodings. Here it is necessary to trade time bounds off against length of encodings.

This paper investigates second-order representations in the sense of Kawamura and Cook for spaces of integrable functions that regularly show up in analysis. It builds upon prior work about the space of continuous functions on the unit interval: Kawamura and Cook introduced a representation inducing the right complexity classes and proved that it is the weakest second-order representation such that evaluation is polynomial-time computable. The first part of this paper provides a similar representation for the space of integrable functions on a bounded subset of Euclidean space: The weakest representation rendering integration over boxes is polynomial-time computable. In contrast to the representation of continuous functions, however, this representation turns out to be discontinuous with respect to both the norm and the weak topology. The second part modifies the representation to be continuous and generalizes it to Lp-spaces. The arising representations are proven to be computably equivalent to the standard representations of these spaces as metric spaces and to still render integration polynomial-time computable. The family is extended to cover Sobolev spaces on the unit interval, where less basic operations like differentiation and some Sobolev embeddings are shown to be polynomial-time computable. Finally as a further justification quantitative versions of the Arzel\`a-Ascoli and Fr\'echet-Kolmogorov Theorems are presented and used to argue that these representations fulfill a minimality condition. To provide tight bounds for the Fr\'echet-Kolmogorov Theorem, a form of exponential time computability of the norm of Lp is proven.

The last years have seen an increasing interest in classifying (existence claims in) classical mathematical theorems according to their strength. We pursue this goal from the refined perspective of computational complexity. Specifically, we establish that rigorously solving the Dirichlet Problem for Poisson's Equation is in a precise sense ‘complete’ for the complexity class ${\#\mathcal{P}}$ and thus as hard or easy as parametric Riemann integration (Friedman 1984; Ko 1991.Complexity Theory of Real Functions).

We promote the theory of computational complexity on metric spaces: as natural common generalization of (i) the classical discrete setting of integers, binary strings, graphs etc. as well as of (ii) the bit-complexity theory on real numbers and functions according to Friedman, Ko (1982ff), Cook, Braverman et al.; as (iii) resource-bounded refinement of the theories of computability on, and representations of, continuous universes by Pour-El&Richards (1989) and Weihrauch (1993ff); and as (iv) computational perspective on quantitative concepts from classical Analysis: Our main results relate (i.e. upper and lower bound) Kolmogorov's entropy of a compact metric space X polynomially to the uniform relativized complexity of approximating various families of continuous functions on X. The upper bounds are attained by carefully crafted oracles and bit-cost analyses of algorithms perusing them. They all employ the same representation (i.e. encoding, as infinite binary sequences, of the elements) of such spaces, which thus may be of own interest. The lower bounds adapt adversary arguments from unit-cost Information-Based Complexity to the bit model. They extend to, and indicate perhaps surprising limitations even of, encodings via binary string functions (rather than sequences) as introduced by Kawamura&Cook (SToC'2010, §3.4). These insights offer some guidance towards suitable notions of complexity for higher types.