Verified computations

Dawood, Hend, and Nefertiti Megahed. "Automatic Differentiation of Uncertainties: An Interval Computational Differentiation for First and Higher Derivatives with Implementation." PeerJ Computer Science 9, no. 5 (2023): e1301. Abstractpeerjcs1301_dawood.pdfWebsite

Acquiring reliable knowledge amidst uncertainty is a topical issue of modern science. Interval mathematics has proved to be of central importance in coping with uncertainty and imprecision. Algorithmic differentiation, being superior to both numeric and symbolic differentiation, is nowadays one of the most celebrated techniques in the field of computational mathematics. In this connexion, laying out a concrete theory of interval differentiation arithmetic, combining subtlety of ordinary algorithmic differentiation with power and reliability of interval mathematics, can extend real differentiation arithmetic so markedly both in method and objective, and can so far surpass it in power as well as applicability. This article is intended to lay out a systematic theory of dyadic interval differentiation numbers that wholly addresses first and higher order automatic derivatives under uncertainty. We begin by axiomatizing a differential interval algebra and then we present the notion of an interval extension of a family of real functions, together with some analytic notions of interval functions. Next, we put forward an axiomatic theory of interval differentiation arithmetic, as a two-sorted extension of the theory of a differential interval algebra, and provide the proofs for its categoricity and consistency. Thereupon, we investigate the ensuing structure and show that it constitutes a multiplicatively non-associative S-semiring in which multiplication is subalternative and flexible. Finally, we show how to computationally realize interval automatic differentiation. Many examples are given, illustrating automatic differentiation of interval functions and families of real functions.