We establish Diophantine hardness results for the decidability of the Positivity Problem for exponential-trigonometric polynomials over computable discrete subfields of the real numbers, and for related questions. We show that any algorithm for deciding either non-negativity, eventual non-negativity, the existence of a zero, or the existence of infinitely many zeros of exponential-trigonometric polynomials over a computable discrete subfield K of the reals containing the number π can be translated into an algorithm for computing the irrationality exponents of all elements of K. As a consequence, we exhibit a computable discrete subfield K of the reals such that all of the aforementioned questions about exponential-trigonometric polynomials over K are undecidable. In particular, we provide the first example of a natural generalisation of the Continuous Skolem Problem that is provably undecidable.

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.

We study the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets. We establish a uniform upper bound on the number of iterations it takes for every orbit of a rational matrix to escape a compact semialgebraic set defined over rational data. Our bound is doubly exponential in the ambient dimension, singly exponential in the degrees of the polynomials used to define the semialgebraic set, and singly exponential in the bitsize of the coefficients of these polynomials and the bitsize of the matrix entries. We show that our bound is tight by providing a matching lower bound.

In the author's PhD thesis (2019) universal envelopes were introduced as a tool for studying the continuously obtainable information on discontinuous functions. To any function $f \colon X \to Y$ between $\operatorname{qcb}_0$-spaces one can assign a so-called universal envelope which, in a well-defined sense, encodes all continuously obtainable information on the function. A universal envelope consists of two continuous functions $F \colon X \to L$ and $\xi_L \colon Y \to L$ with values in a $\Sigma$-split injective space $L$. Any continuous function with values in an injective space whose composition with the original function is again continuous factors through the universal envelope. However, it is not possible in general to uniformly compute this factorisation. In this paper we propose the notion of uniform envelopes. A uniform envelope is additionally endowed with a map $u_L \colon L \to \mathcal{O}^2(Y)$ that is compatible with the multiplication of the double powerspace monad $\mathcal{O}^2$ in a certain sense. This yields for every continuous map with values in an injective space a choice of uniformly computable extension. Under a suitable condition which we call uniform universality, this extension yields a uniformly computable solution for the above factorisation problem. Uniform envelopes can be endowed with a composition operation. We establish criteria that ensure that the composition of two uniformly universal envelopes is again uniformly universal. These criteria admit a partial converse and we provide evidence that they cannot be easily improved in general. Not every function admits a uniformly universal uniform envelope. We can however assign to every function a canonical envelope that is in some sense as close as possible to a uniform envelope. We obtain a composition theorem similar to the uniform case.

We study decision problems for sequences which obey a second-order holonomic recurrence of the form f(n + 2) = P(n) f(n + 1) + Q(n) f(n) with rational polynomial coefficients, where P is non-constant, Q is non-zero, and the degree of Q is smaller than or equal to that of P. We show that existence of infinitely many zeroes is decidable. We give partial algorithms for deciding the existence of a zero, positivity of all sequence terms, and positivity of all but finitely many sequence terms. If Q does not have a positive integer zero then our algorithms halt on almost all initial values (f(1), f(2)) for the recurrence. We identify a class of recurrences for which our algorithms halt for all initial values. We further identify a class of recurrences for which our algorithms can be extended to total ones.

We study the computational complexity of the Escape Problem for discrete-time linear dynamical systems over compact semialgebraic sets, or equivalently the Termination Problem for affine loops with compact semialgebraic guard sets. Consider the fragment of the theory of the reals consisting of negation-free $\exists \forall$-sentences without strict inequalities. We derive several equivalent characterisations of the associated complexity class which demonstrate its robustness and illustrate its expressive power. We show that the Compact Escape Problem is complete for this class.

We study the decidability of the Skolem Problem, the Positivity Problem, and the Ultimate Positivity Problem for linear recurrences with real number initial values and real number coefficients in the bit-model of real computation. We show that for each problem there exists a correct partial algorithm which halts for all problem instances for which the answer is locally constant, thus establishing that all three problems are as close to decidable as one can expect them to be in this setting. We further show that the algorithms for the Positivity Problem and the Ultimate Positivity Problem halt on almost every instance with respect to the usual Lebesgue measure on Euclidean space. In comparison, the analogous problems for exact rational or real algebraic coefficients are known to be decidable only for linear recurrences of fairly low order.

We consider the problem of synthesising polynomial ranking functions for single-path loops over the reals with continuous semi-algebraic update function and compact semi-algebraic guard set. We show that a loop of this form has a polynomial ranking function if and only if it terminates. We further show that termination is decidable for such loops in the special case where the update function is affine.

The basic notions of quantum mechanics are formulated in terms of separable infinite dimensional Hilbert space $\mathcal{H}$. In terms of the Hilbert lattice $\mathcal{L}$ of closed linear subspaces of $\mathcal{H}$ the notions of state and observable can be formulated as kinds of measures as in [21]. The aim of this paper is to show that there is a good notion of computability for these data structures in the sense of Weihrauch's Type Two Effectivity (TTE) [26]. Instead of explicitly exhibiting admissible representations for the data types under consideration we show that they do live within the category $\mathbf{QCB}_0$ which is equivalent to the category $\mathbf{AdmRep}$ of admissible representations and continuously realizable maps between them. For this purpose in case of observables we have to replace measures by valuations which allows us to prove an effective version of von Neumann's Spectral Theorem.