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.

Almost all problems in applied mathematics, including the analysis of dynamical systems, deal with spaces of real-valued functions on Euclidean domains in their formulation and solution. In this paper, we describe the the tool Ariadne, which provides a rigorous calculus for working with Euclidean functions. We first introduce the Ariadne framework, which is based on a clean separation of objects as providing exact, effective, validated and approximate information. We then discuss the function calculus as implemented in Ariadne, including polynomial function models which are the fundamental class for concrete computations. We then consider solution of some core problems of functional analysis, namely solution of algebraic equations and differential equations, and briefly discuss their use for the analysis of hybrid systems. We will give examples of C++ and Python code for performing the various calculations. Finally, we will discuss progress on extensions, including improvements to the function calculus and extensions to more complicated classes of system.

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.

Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either only discrete or only continuous models. A good framework for hybrid systems should support their compositional description and analysis, since commonly systems are specified by a composition of smaller subsystems, to cope with the complexity of their monolithic representation. Moreover, since the reachability problem for hybrid systems is undecidable, one should investigate the conditions that guarantee approximate computability of composition, when only approximations to the exact problem data are available.

Abstract Numerical computation is traditionally performed using floating-point arithmetic and truncated forms of infinite series, a methodology which allows for efficient computation at the cost of some accuracy. For most applications, these errors are entirely acceptable and the numerical results are considered trustworthy, but for some operations, we may want to have guarantees that the numerical results are correct, or explicit bounds on the errors. To obtain rigorous calculations, floating-point arithmetic is usually replaced by interval arithmetic and truncation errors are explicitly contained in the result. We may then ask the question of which mathematical operations can be implemented in a way in which the exact result can be approximated to arbitrary known accuracy by a numerical algorithm. This is the subject ofcomputable analysisand forms a theoretical underpinning of rigorous numerical computation. The aim of this article is to provide a straightforward introduction to this subject that is powerful enough to answer questions arising in dynamic system theory.

Increasingly, multiple parallel omics datasets are collected from biological samples. Integrating these datasets for classification is an open area of research. Additionally, whilst multiple datasets may be available for the training samples, future samples may only be measured by a single technology requiring methods which do not rely on the presence of all datasets for sample prediction. This enables us to directly compare the protein and the gene profiles. New samples with just one set of measurements (e.g., just protein) can then be mapped to this latent common space where classification is performed. Using this approach, we achieved an improvement of up to 12 percent in accuracy when classifying samples based on their protein measurements compared with baseline methods which were trained on the protein data alone. We illustrate that the additional inclusion of the gene expression or protein expression in the training process enabled the separation between the classes to become clearer.

In this paper we consider the computation of reachable, viable and invariant sets for discrete-time systems. We use the framework of type-two effectivity, in which computations are performed by Turing machines with infinite input and output tapes, with the representations of computable topology. We see that the reachable set is lower-semicomputable, and the viability and invariance kernels are upper-semicomputable. We then define an upper-semicomputable over-approximation to the reachable set, and lower-semicomputable under-approximations to the viability and invariance kernels, and show that these approximations are optimal.