Average Error: 0.2 → 0.0
Time: 19.5s
Precision: binary64
\[\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(b \cdot b\right)\right) - 1 \]
↓
\[{\left(\mathsf{hypot}\left(a, b\right)\right)}^{4} + \mathsf{fma}\left(b, b \cdot 4, -1\right) \]
\left({\left(a \cdot a + b \cdot b\right)}^{2} + 4 \cdot \left(b \cdot b\right)\right) - 1
↓
{\left(\mathsf{hypot}\left(a, b\right)\right)}^{4} + \mathsf{fma}\left(b, b \cdot 4, -1\right)

(FPCore (a b)
 :precision binary64
 (- (+ (pow (+ (* a a) (* b b)) 2.0) (* 4.0 (* b b))) 1.0))
↓
(FPCore (a b)
 :precision binary64
 (+ (pow (hypot a b) 4.0) (fma b (* b 4.0) -1.0)))
double code(double a, double b) {
	return (pow(((a * a) + (b * b)), 2.0) + (4.0 * (b * b))) - 1.0;
}
↓
double code(double a, double b) {
	return pow(hypot(a, b), 4.0) + fma(b, (b * 4.0), -1.0);
}

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(b \cdot b\right)\right) - 1 \]

  2. Simplified0.0

    \[\leadsto \color{blue}{{\left(\mathsf{hypot}\left(a, b\right)\right)}^{4} + \mathsf{fma}\left(b, b \cdot 4, -1\right)} \]
    Proof
    (-.f64 (+.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) 2) (*.f64 4 (*.f64 b b))) 1): 0 points increase in error, 0 points decrease in error
    (Rewrite=> sub-neg_binary64 (+.f64 (+.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) 2) (*.f64 4 (*.f64 b b))) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (Rewrite=> associate-+l+_binary64 (+.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) 2) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1)))): 2 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 2 2)) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 2 2)))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (Rewrite=> metadata-eval 1)) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 2 2))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)))) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 2 2))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2))) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (Rewrite=> metadata-eval 1))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2))) (Rewrite=> unpow1_binary64 (+.f64 (*.f64 a a) (*.f64 b b)))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite=> associate-*l*_binary64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (+.f64 (*.f64 a a) (*.f64 b b))))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 3 points increase in error, 24 points decrease in error
    (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (+.f64 (*.f64 a a) (*.f64 b b))) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (Rewrite<= unpow1_binary64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) 1))) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (Rewrite=> sqr-pow_binary64 (*.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2))))) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 (Rewrite=> cube-unmult_binary64 (pow.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) 3)) (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 5 points increase in error, 9 points decrease in error
    (+.f64 (Rewrite=> pow-plus_binary64 (pow.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (/.f64 1 2)) (+.f64 3 1))) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 1 points increase in error, 22 points decrease in error
    (+.f64 (pow.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) (Rewrite=> metadata-eval 1/2)) (+.f64 3 1)) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (Rewrite=> unpow1/2_binary64 (sqrt.f64 (+.f64 (*.f64 a a) (*.f64 b b)))) (+.f64 3 1)) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (Rewrite=> hypot-def_binary64 (hypot.f64 a b)) (+.f64 3 1)) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (hypot.f64 a b) (Rewrite=> metadata-eval 4)) (+.f64 (*.f64 4 (*.f64 b b)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (hypot.f64 a b) 4) (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 4 (*.f64 b b)) 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (hypot.f64 a b) 4) (-.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 4 b) b)) 1)): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (hypot.f64 a b) 4) (-.f64 (Rewrite=> *-commutative_binary64 (*.f64 b (*.f64 4 b))) 1)): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (hypot.f64 a b) 4) (Rewrite=> fma-neg_binary64 (fma.f64 b (*.f64 4 b) (neg.f64 1)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (hypot.f64 a b) 4) (fma.f64 b (Rewrite=> *-commutative_binary64 (*.f64 b 4)) (neg.f64 1))): 0 points increase in error, 0 points decrease in error
    (+.f64 (pow.f64 (hypot.f64 a b) 4) (fma.f64 b (*.f64 b 4) (Rewrite=> metadata-eval -1))): 0 points increase in error, 0 points decrease in error

  3. Final simplification0.0

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

Reproduce

herbie shell --seed 2022160 
(FPCore (a b)
  :name "Bouland and Aaronson, Equation (26)"
  :precision binary64
  (- (+ (pow (+ (* a a) (* b b)) 2.0) (* 4.0 (* b b))) 1.0))