# Hyperdual Numbers and Forward Differentiation

 Title: Hyperdual Numbers and Forward Differentiation Authors: Filip Smola and Jacques Fleuriot Submission date: 2021-12-31 Abstract: Hyperdual numbers are ones with a real component and a number of infinitesimal components, usually written as $a_0 + a_1 \cdot \epsilon_1 + a_2 \cdot \epsilon_2 + a_3 \cdot \epsilon_1\epsilon_2$. They have been proposed by Fike and Alonso in an approach to automatic differentiation. In this entry we formalise hyperdual numbers and their application to forward differentiation. We show them to be an instance of multiple algebraic structures and then, along with facts about twice-differentiability, we define what we call the hyperdual extensions of functions on real-normed fields. This extension formally represents the proposed way that the first and second derivatives of a function can be automatically calculated. We demonstrate it on the standard logistic function $f(x) = \frac{1}{1 + e^{-x}}$ and also reproduce the example analytic function $f(x) = \frac{e^x}{\sqrt{sin(x)^3 + cos(x)^3}}$ used for demonstration by Fike and Alonso. BibTeX: @article{Hyperdual-AFP, author = {Filip Smola and Jacques Fleuriot}, title = {Hyperdual Numbers and Forward Differentiation}, journal = {Archive of Formal Proofs}, month = dec, year = 2021, note = {\url{https://isa-afp.org/entries/Hyperdual.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.