Bouland and Aaronson, Equation (25)

Average Accuracy: 99.7% → 100.0%

Time: 10.6s

Precision: binary64

Cost: 39488

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(\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{+.f64}\left(1, a\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(3, a\right)\right)\right)\right)\right)\right), 1\right) \]

↓

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

FPCore

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

↓

(FPCore (a b)
 :precision binary64
 (+.f64
  (fma.f64
   4
   (fma.f64 a (fma.f64 a a a) (*.f64 b (*.f64 b (fma.f64 a -3 1))))
   (pow.f64 (hypot.f64 a 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(\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{+.f64}\left(1, a\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(3, a\right)\right)\right)\right)\right)\right), 1\right) \]

2. Simplified 100.0%

   \[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{fma.f64}\left(4, \mathsf{fma.f64}\left(a, \mathsf{fma.f64}\left(a, a, a\right), \mathsf{*.f64}\left(b, \mathsf{*.f64}\left(b, \mathsf{fma.f64}\left(a, -3, 1\right)\right)\right)\right), \mathsf{pow.f64}\left(\mathsf{hypot.f64}\left(a, b\right), 4\right)\right), -1\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(\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{+.f64}\left(1, a\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(3, a\right)\right)\right)\right)\right)\right), 1\right) \]

   sub-neg [=>] 99.7

   \[ \color{blue}{\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(\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{+.f64}\left(1, a\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(3, a\right)\right)\right)\right)\right)\right), \mathsf{neg.f64}\left(1\right)\right)} \]

3. Final simplification 100.0%

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

Alternatives

Alternative 1
Accuracy	99.7%
Cost	8320

\[\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(\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{+.f64}\left(a, 1\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(a, 3\right)\right)\right)\right)\right)\right), -1\right) \]

Alternative 2
Accuracy	99.6%
Cost	7936

\[\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(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{+.f64}\left(a, 1\right)\right)\right)\right)\right), -1\right) \]

Alternative 3
Accuracy	97.7%
Cost	7817

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

Alternative 4
Accuracy	97.8%
Cost	7680

\[\begin{array}{l} t_0 := \mathsf{+.f64}\left(\mathsf{*.f64}\left(a, a\right), \mathsf{*.f64}\left(b, b\right)\right)\\ \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(t_0, 2\right), \mathsf{*.f64}\left(4, t_0\right)\right), -1\right) \end{array} \]

Alternative 5
Accuracy	97.8%
Cost	7556

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

Alternative 6
Accuracy	96.5%
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(a, \mathsf{*.f64}\left(4, a\right)\right)\right), -1\right) \]

Alternative 7
Accuracy	96.6%
Cost	7300

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, a\right), \frac{4722366482869645}{2361183241434822606848}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(b, 4\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(b, b\right)\right)\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 3\right), \mathsf{+.f64}\left(4, a\right)\right), -1\right)\\ \end{array} \]

Alternative 8
Accuracy	96.5%
Cost	7236

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, a\right), \frac{4722366482869645}{2361183241434822606848}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, \mathsf{*.f64}\left(b, \mathsf{fma.f64}\left(b, b, 4\right)\right)\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 3\right), \mathsf{+.f64}\left(4, a\right)\right), -1\right)\\ \end{array} \]

Alternative 9
Accuracy	95.9%
Cost	7177

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a, \frac{-23}{2}\right) \lor \neg \mathsf{<=.f64}\left(a, \frac{496910556692507}{2923003274661805836407369665432566039311865085952}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 3\right), \mathsf{+.f64}\left(4, a\right)\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{+.f64}\left(4, \mathsf{*.f64}\left(a, -12\right)\right)\right)\right), -1\right)\\ \end{array} \]

Alternative 10
Accuracy	95.0%
Cost	6921

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(a, \frac{-5626256942481413}{4611686018427387904}\right) \lor \neg \mathsf{<=.f64}\left(a, \frac{496910556692507}{2923003274661805836407369665432566039311865085952}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{pow.f64}\left(a, 4\right), -1\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{+.f64}\left(4, \mathsf{*.f64}\left(a, -12\right)\right)\right)\right), -1\right)\\ \end{array} \]

Alternative 11
Accuracy	81.7%
Cost	960

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

Alternative 12
Accuracy	81.7%
Cost	704

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

Alternative 13
Accuracy	80.4%
Cost	576

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

Alternative 14
Accuracy	64.7%
Cost	448

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

Reproduce

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