Bouland and Aaronson, Equation (26)

Average Accuracy: 99.7% → 100.0%

Time: 3.5s

Precision: binary64

Cost: 19776

Math

\[\mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), 2\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right)\right), 1\right) \]

↓

\[\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{hypot.f64}\left(a, b\right), 4\right), \mathsf{fma.f64}\left(b, \mathsf{*.f64}\left(b, 4\right), -1\right)\right) \]

FPCore

(FPCore (a b)
 :precision binary64
 (-.f64
  (+.f64 (pow.f64 (+.f64 (*.f64 a a) (*.f64 b b)) 2) (*.f64 4 (*.f64 b b)))
  1))

↓

(FPCore (a b)
 :precision binary64
 (+.f64 (pow.f64 (hypot.f64 a b) 4) (fma.f64 b (*.f64 b 4) -1)))

Derivation

1. Initial program 99.7%

   \[\mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), 2\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right)\right), 1\right) \]

2. Simplified 100.0%

   \[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{hypot.f64}\left(a, b\right), 4\right), \mathsf{fma.f64}\left(b, \mathsf{*.f64}\left(b, 4\right), -1\right)\right)} \]
   Proof

   [Start] 99.7	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), 2\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right)\right), 1\right) \]
   associate--l+ [=>] 99.7	\[ \color{blue}{\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), 2\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right), 1\right)\right)} \]
   unpow2 [=>] 99.7	\[ \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right)\right)}, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right), 1\right)\right) \]
   unpow1 [<=] 99.7	\[ \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \color{blue}{\mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), 1\right)}\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right), 1\right)\right) \]
   sqr-pow [=>] 99.7	\[ \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{/.f64}\left(1, 2\right)\right)\right)}\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right), 1\right)\right) \]
   associate-*r* [=>] 99.8	\[ \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{/.f64}\left(1, 2\right)\right)\right)}, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right), 1\right)\right) \]

3. Final simplification 100.0%

   \[\leadsto \mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{hypot.f64}\left(a, b\right), 4\right), \mathsf{fma.f64}\left(b, \mathsf{*.f64}\left(b, 4\right), -1\right)\right) \]

Alternatives

Alternative 1
Accuracy	99.7%
Cost	7424

\[\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right), 2\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right)\right), -1\right) \]

Alternative 2
Accuracy	97.5%
Cost	7305

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(b, -1950\right) \lor \neg \mathsf{<=.f64}\left(b, \frac{2476979795053773}{2251799813685248}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{+.f64}\left(t_0, \mathsf{pow.f64}\left(b, 4\right)\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{+.f64}\left(t_0, \mathsf{pow.f64}\left(a, 4\right)\right), -1\right)\\ \end{array} \]

Alternative 3
Accuracy	83.4%
Cost	7040

\[\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right), \mathsf{pow.f64}\left(a, 4\right)\right), -1\right) \]

Alternative 4
Accuracy	82.1%
Cost	6656

\[\mathsf{+.f64}\left(\mathsf{pow.f64}\left(a, 4\right), -1\right) \]

Alternative 5
Accuracy	65.4%
Cost	448

\[\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, \mathsf{*.f64}\left(b, 4\right)\right), -1\right) \]

Reproduce

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