### 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.

### License

BSD License

### Topics

- Mathematics/Algebra
- Mathematics/Analysis

### Session Hyperdual

- Hyperdual
- TwiceFieldDifferentiable
- HyperdualFunctionExtension
- LogisticFunction
- AnalyticTestFunction

## Cite

×

Hyperdual-AFP

    @article{Hyperdual-AFP,
      author  = {Filip Smola and Jacques D. Fleuriot},
      title   = {Hyperdual Numbers and Forward Differentiation},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Hyperdual.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jan 5, 2022 : Isabelle2021-1