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 twicedifferentiability, we define what we call
the hyperdual extensions of functions on realnormed 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{HyperdualAFP,
author = {Filip Smola and Jacques Fleuriot},
title = {Hyperdual Numbers and Forward Differentiation},
journal = {Archive of Formal Proofs},
month = dec,
year = 2021,
note = {\url{https://isaafp.org/entries/Hyperdual.html},
Formal proof development},
ISSN = {2150914x},
}
