We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the `precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.

ksmt is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this article we investigate properties of the ksmt calculus and show that it is a δ-complete decision procedure for bounded problems. For that purpose we provide concrete algorithms computing linearisations based on either uniform or local moduli of continuity of non-linear functions. The latter method is called local linearisation and is shown to have desirable properties sufficient for termination and which also allow for more efficient treatment of non-linear constraints. Our methods for constructing linearisations are based on computable analysis, in particular we introduce the Cauchy-compatible compact representation of reals and prove its names to be locally compact, allowing for more efficient computation of local linearisations while maintaining δ-completeness.

Abstract is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the calculus and show that it is a $$\delta $$ δ -complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.

Numerical instability is a well-known problem that may cause serious runtime failures. This paper discusses the reason of instability in software development process, and presents a toolchain that not only detects the potential instability in software, but also diagnoses the reason for such instability. We classify the reason of instability into two categories. When it is introduced by software requirements, we call the instability caused by problem . In this case, it cannot be avoided by improving software development, but requires inspecting the requirements, especially the underlying mathematical properties. Otherwise, we call the instability caused by practice. We design our toolchain as four loosely-coupled tools, which combine stochastic arithmetic with infinite-precision testing. Each tool in our toolchain can be configured with different strategies according to the properties of the analyzed software. We evaluate our toolchain on subjects from literature. The results show that it effectively detects and separates the instabilities caused by problems from others. We also conduct an evaluation on the latest version of GNU Scientific Library, and the toolchain finds a few real bugs in the well-maintained and widely deployed numerical library. With the help of our toolchain, we report the details and fixing advices to the GSL buglist.

The synthesis of (discrete) Complexity Theory with Recursive Analysis provides a quantitative algorithmic foundation to calculations over real numbers, sequences, and functions by approximation up to prescribable absolute error 1/2n (roughly corresponding to n binary digits after the radix point). In this sense Friedman and Ko have shown the seemingly simple operators of maximization and integration 'complete' for the standard complexity classes NP and #P — even when restricted to smooth (=C∞) arguments. Analytic polynomial-time computable functions on the other hand are known to get mapped to polynomial-time computable functions: non-uniformly, that is, disregarding dependences other than on the output precision n. The present work investigates the uniform parameterized complexity of natural operators Λ on subclasses of smooth functions: evaluation, pointwise addition and multiplication, (iterated) differentiation, integration, and maximization. We identify natural integer parameters k=k(f) which, when given as enrichment to approximations to the function argument f, permit to computably produce approximations to Λ(f); and we explore the asymptotic worst-case running time sufficient and necessary for such computations in terms of the output precision n and said k. It turns out that Maurice Gevrey's 1918 classical hierarchy climbing from analytic to (just below) smooth functions provides for a quantitative gauge of the uniform computational complexity of maximization and integration that, non-uniformly, exhibits the phase transition from tractable (i.e. polynomial-time) to intractable (in the sense of NP-'hardness'). Our proof methods involve Hard Analysis, Approximation Theory, and an adaptation of Information-Based Complexity to the bit model.

We consider the solution of initial value problems within the context of hybrid systems and emphasise the use of high precision approximations (in software for exact real arithmetic). We propose a novel algorithm for the computation of trajectories up to the area where discontinuous jumps appear, applicable for holomorphic flow functions. Examples with a prototypical implementation illustrate that the algorithm might provide results with higher precision than well-known ODE solvers at a similar computation time.