Rigorous Function Calculi in Ariadne
Pieter Collins, Luca Geretti, Sanja Zivanovic Gonzalez, Davide Bresolin, Tiziano Villa
TL;DR
Ariadne delivers a rigorous, general-purpose calculus for real-valued functions on Euclidean domains by embedding computable analysis into a software kernel. It combines interval arithmetic, Taylor-models, and validated operations to provide guaranteed results for algebraic and differential equations, including hybrid systems. The paper details the low-level data types, function-calculus machinery, and solver implementations, complemented by C++/Python examples on the Fitzhugh-Nagumo model. Its modular design paves the way for extensions to alternative bases, differentiable and measurable function classes, and more complex dynamical systems, enabling provably correct analysis and verification in continuous and hybrid contexts.
Abstract
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.