Bouland and Aaronson, Equation (24)

Average Error: 0.2 → 0.0

Time: 9.2s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1\]

↓

\[\mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\left(\mathsf{hypot}\left(a, b\right)\right)}^{\left(2 + 2\right)}\right) - 1\]

C

double f(double a, double b) {
        double r311467 = a;
        double r311468 = r311467 * r311467;
        double r311469 = b;
        double r311470 = r311469 * r311469;
        double r311471 = r311468 + r311470;
        double r311472 = 2.0;
        double r311473 = pow(r311471, r311472);
        double r311474 = 4.0;
        double r311475 = 1.0;
        double r311476 = r311475 - r311467;
        double r311477 = r311468 * r311476;
        double r311478 = 3.0;
        double r311479 = r311478 + r311467;
        double r311480 = r311470 * r311479;
        double r311481 = r311477 + r311480;
        double r311482 = r311474 * r311481;
        double r311483 = r311473 + r311482;
        double r311484 = r311483 - r311475;
        return r311484;
}

↓

double f(double a, double b) {
        double r311485 = a;
        double r311486 = r311485 * r311485;
        double r311487 = 1.0;
        double r311488 = r311487 - r311485;
        double r311489 = b;
        double r311490 = r311489 * r311489;
        double r311491 = 3.0;
        double r311492 = r311491 + r311485;
        double r311493 = r311490 * r311492;
        double r311494 = fma(r311486, r311488, r311493);
        double r311495 = 4.0;
        double r311496 = hypot(r311485, r311489);
        double r311497 = 2.0;
        double r311498 = r311497 + r311497;
        double r311499 = pow(r311496, r311498);
        double r311500 = fma(r311494, r311495, r311499);
        double r311501 = r311500 - r311487;
        return r311501;
}

Error

Bits error versus a

Bits error versus b

Derivation

1. Initial program 0.2

   \[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(\left(a \cdot a\right) \cdot \left(1 - a\right) + \left(b \cdot b\right) \cdot \left(3 + a\right)\right)\right) - 1\]

2. Simplified 0.2

   \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\left(\mathsf{fma}\left(a, a, b \cdot b\right)\right)}^{2}\right) - 1}\]
3. Using strategy rm

4. Applied add-sqr-sqrt 0.2

   \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\color{blue}{\left(\sqrt{\mathsf{fma}\left(a, a, b \cdot b\right)} \cdot \sqrt{\mathsf{fma}\left(a, a, b \cdot b\right)}\right)}}^{2}\right) - 1\]

5. Applied unpow-prod-down 0.2

   \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, \color{blue}{{\left(\sqrt{\mathsf{fma}\left(a, a, b \cdot b\right)}\right)}^{2} \cdot {\left(\sqrt{\mathsf{fma}\left(a, a, b \cdot b\right)}\right)}^{2}}\right) - 1\]

6. Simplified 0.2

   \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, \color{blue}{{\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}} \cdot {\left(\sqrt{\mathsf{fma}\left(a, a, b \cdot b\right)}\right)}^{2}\right) - 1\]

7. Simplified 0.2

   \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2} \cdot \color{blue}{{\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}}\right) - 1\]
8. Using strategy rm

9. Applied *-un-lft-identity 0.2

   \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2} \cdot {\color{blue}{\left(1 \cdot \mathsf{hypot}\left(a, b\right)\right)}}^{2}\right) - 1\]

10. Applied unpow-prod-down 0.2

    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2} \cdot \color{blue}{\left({1}^{2} \cdot {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}\right)}\right) - 1\]

11. Applied *-un-lft-identity 0.2

    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\color{blue}{\left(1 \cdot \mathsf{hypot}\left(a, b\right)\right)}}^{2} \cdot \left({1}^{2} \cdot {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}\right)\right) - 1\]

12. Applied unpow-prod-down 0.2

    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, \color{blue}{\left({1}^{2} \cdot {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}\right)} \cdot \left({1}^{2} \cdot {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}\right)\right) - 1\]

13. Applied swap-sqr 0.2

    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, \color{blue}{\left({1}^{2} \cdot {1}^{2}\right) \cdot \left({\left(\mathsf{hypot}\left(a, b\right)\right)}^{2} \cdot {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}\right)}\right) - 1\]

14. Simplified 0.2

    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, \color{blue}{1} \cdot \left({\left(\mathsf{hypot}\left(a, b\right)\right)}^{2} \cdot {\left(\mathsf{hypot}\left(a, b\right)\right)}^{2}\right)\right) - 1\]

15. Simplified 0.0

    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, 1 \cdot \color{blue}{{\left(\mathsf{hypot}\left(a, b\right)\right)}^{\left(2 + 2\right)}}\right) - 1\]

16. Final simplification 0.0

    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, 1 - a, \left(b \cdot b\right) \cdot \left(3 + a\right)\right), 4, {\left(\mathsf{hypot}\left(a, b\right)\right)}^{\left(2 + 2\right)}\right) - 1\]

Reproduce

herbie shell --seed 2020047 +o rules:numerics
(FPCore (a b)
  :name "Bouland and Aaronson, Equation (24)"
  :precision binary64
  (- (+ (pow (+ (* a a) (* b b)) 2) (* 4 (+ (* (* a a) (- 1 a)) (* (* b b) (+ 3 a))))) 1))