sqrt times

Average Accuracy: 99.2% → 99.6%

Time: 1.9s

Precision: binary64

Cost: 832

Math

\[\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{sqrt.f64}\left(x\right)\right) \]

↓

\[\mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\frac{1}{8}, x\right), \mathsf{/.f64}\left(\frac{1}{16}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right) \]

FPCore

(FPCore (x) :precision binary64 (*.f64 (sqrt.f64 (-.f64 x 1)) (sqrt.f64 x)))

↓

(FPCore (x)
 :precision binary64
 (-.f64 (+.f64 x -1/2) (+.f64 (/.f64 1/8 x) (/.f64 1/16 (*.f64 x x)))))

Derivation

1. Initial program 99.2%

   \[\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{sqrt.f64}\left(x\right)\right) \]

2. Taylor expanded in x around inf 99.6%

   \[\leadsto \color{blue}{\mathsf{\_.f64}\left(x, \mathsf{+.f64}\left(\frac{1}{2}, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right), \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right)} \]

3. Simplified 99.6%

   \[\leadsto \color{blue}{\mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\frac{1}{8}, x\right), \mathsf{/.f64}\left(\frac{1}{16}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)} \]
   Proof

   [Start] 99.6	\[ \mathsf{\_.f64}\left(x, \mathsf{+.f64}\left(\frac{1}{2}, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right), \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right) \]
   associate--r+ [=>] 99.6	\[ \color{blue}{\mathsf{\_.f64}\left(\mathsf{\_.f64}\left(x, \frac{1}{2}\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right), \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(1, x\right)\right)\right)\right)} \]
   sub-neg [=>] 99.6	\[ \mathsf{\_.f64}\left(\color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(\frac{1}{2}\right)\right)}, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right), \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(1, x\right)\right)\right)\right) \]
   metadata-eval [=>] 99.6	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \color{blue}{\frac{-1}{2}}\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right), \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(1, x\right)\right)\right)\right) \]
   +-commutative [=>] 99.6	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(1, x\right)\right), \mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right)\right)}\right) \]
   associate-*r/ [=>] 99.6	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{1}{8}, 1\right), x\right)}, \mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right)\right)\right) \]
   metadata-eval [=>] 99.6	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\color{blue}{\frac{1}{8}}, x\right), \mathsf{*.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(x, 2\right)\right)\right)\right)\right) \]
   associate-*r/ [=>] 99.6	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\frac{1}{8}, x\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{1}{16}, 1\right), \mathsf{pow.f64}\left(x, 2\right)\right)}\right)\right) \]
   metadata-eval [=>] 99.6	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\frac{1}{8}, x\right), \mathsf{/.f64}\left(\color{blue}{\frac{1}{16}}, \mathsf{pow.f64}\left(x, 2\right)\right)\right)\right) \]
   unpow2 [=>] 99.6	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\frac{1}{8}, x\right), \mathsf{/.f64}\left(\frac{1}{16}, \color{blue}{\mathsf{*.f64}\left(x, x\right)}\right)\right)\right) \]

4. Final simplification 99.6%

   \[\leadsto \mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\frac{1}{8}, x\right), \mathsf{/.f64}\left(\frac{1}{16}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right) \]

Alternatives

Alternative 1
Accuracy	99.4%
Cost	448

\[\mathsf{\_.f64}\left(\mathsf{+.f64}\left(x, \frac{-1}{2}\right), \mathsf{/.f64}\left(\frac{1}{8}, x\right)\right) \]

Alternative 2
Accuracy	99.1%
Cost	192

\[\mathsf{\_.f64}\left(x, \frac{1}{2}\right) \]

Alternative 3
Accuracy	98.0%
Cost	64

\[x \]

Reproduce

herbie shell --seed 2023144 
(FPCore (x)
  :name "sqrt times"
  :precision binary64
  (* (sqrt (- x 1.0)) (sqrt x)))