Octave 3.8, jcobi/4, as called

Average Accuracy: 27.9% → 99.5%

Time: 3.5s

Precision: binary64

Cost: 576

\[i > 0\]

Math

\[\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right)\right) \]

↓

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

FPCore

(FPCore (i)
 :precision binary64
 (/.f64
  (/.f64 (*.f64 (*.f64 i i) (*.f64 i i)) (*.f64 (*.f64 2 i) (*.f64 2 i)))
  (-.f64 (*.f64 (*.f64 2 i) (*.f64 2 i)) 1)))

↓

(FPCore (i) :precision binary64 (/.f64 1/4 (+.f64 4 (/.f64 -1 (*.f64 i i)))))

Derivation

1. Initial program 27.9%

   \[\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right)\right) \]

2. Simplified 92.4%

   \[\leadsto \color{blue}{\mathsf{/.f64}\left(\frac{1}{4}, \mathsf{\_.f64}\left(4, \mathsf{/.f64}\left(i, \mathsf{pow.f64}\left(i, 3\right)\right)\right)\right)} \]
   Proof

   [Start] 27.9	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right)\right) \]
   times-frac [=>] 75.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(2, i\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(2, i\right)\right)\right)}, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right)\right) \]
   associate-/l* [=>] 75.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(2, i\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(2, i\right)\right)\right)\right)} \]
   associate-/l* [=>] 75.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(i, \mathsf{/.f64}\left(\mathsf{*.f64}\left(2, i\right), i\right)\right)}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(2, i\right)\right)\right)\right) \]
   associate-/l/ [=>] 75.1	\[ \color{blue}{\mathsf{/.f64}\left(i, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(i, i\right), \mathsf{*.f64}\left(2, i\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(2, i\right), i\right)\right)\right)} \]
   associate-/r/ [=>] 74.6	\[ \mathsf{/.f64}\left(i, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(2, i\right)\right)}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(2, i\right), i\right)\right)\right) \]
   associate-/l* [=>] 74.6	\[ \mathsf{/.f64}\left(i, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(2, i\right)\right), \color{blue}{\mathsf{/.f64}\left(2, \mathsf{/.f64}\left(i, i\right)\right)}\right)\right) \]
   *-inverses [=>] 74.6	\[ \mathsf{/.f64}\left(i, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(2, i\right)\right), \mathsf{/.f64}\left(2, \color{blue}{1}\right)\right)\right) \]
   metadata-eval [=>] 74.6	\[ \mathsf{/.f64}\left(i, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(2, i\right)\right), \color{blue}{2}\right)\right) \]
   associate-*l* [=>] 74.6	\[ \mathsf{/.f64}\left(i, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{*.f64}\left(i, i\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), 2\right)\right)}\right) \]
   *-commutative [<=] 74.6	\[ \mathsf{/.f64}\left(i, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), 2\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{*.f64}\left(i, i\right)\right)\right)}\right) \]
   associate-/r* [=>] 74.7	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(i, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), 2\right)\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(2, i\right), \mathsf{*.f64}\left(2, i\right)\right), 1\right), \mathsf{*.f64}\left(i, i\right)\right)\right)} \]

3. Taylor expanded in i around 0 99.5%

   \[\leadsto \mathsf{/.f64}\left(\frac{1}{4}, \mathsf{\_.f64}\left(4, \color{blue}{\mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(i, 2\right)\right)}\right)\right) \]

4. Simplified 99.5%

   \[\leadsto \mathsf{/.f64}\left(\frac{1}{4}, \mathsf{\_.f64}\left(4, \color{blue}{\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(i, i\right)\right)}\right)\right) \]
   Proof

   [Start] 99.5	\[ \mathsf{/.f64}\left(\frac{1}{4}, \mathsf{\_.f64}\left(4, \mathsf{/.f64}\left(1, \mathsf{pow.f64}\left(i, 2\right)\right)\right)\right) \]
   unpow2 [=>] 99.5	\[ \mathsf{/.f64}\left(\frac{1}{4}, \mathsf{\_.f64}\left(4, \mathsf{/.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(i, i\right)}\right)\right)\right) \]

5. Final simplification 99.5%

   \[\leadsto \mathsf{/.f64}\left(\frac{1}{4}, \mathsf{+.f64}\left(4, \mathsf{/.f64}\left(-1, \mathsf{*.f64}\left(i, i\right)\right)\right)\right) \]

Alternatives

Alternative 1
Accuracy	99.2%
Cost	708

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(i, i\right), \frac{3602879701896397}{9007199254740992}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(i, i\right), \frac{-1}{4}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{+.f64}\left(\frac{1}{16}, \mathsf{/.f64}\left(\frac{1}{64}, \mathsf{*.f64}\left(i, i\right)\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	98.9%
Cost	580

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(i, i\right), \frac{3602879701896397}{9007199254740992}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(i, i\right), \frac{-1}{4}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{16}\\ \end{array} \]

Alternative 3
Accuracy	50.8%
Cost	64

\[\frac{1}{16} \]

Reproduce

herbie shell --seed 2023144 
(FPCore (i)
  :name "Octave 3.8, jcobi/4, as called"
  :precision binary64
  :pre (> i 0.0)
  (/ (/ (* (* i i) (* i i)) (* (* 2.0 i) (* 2.0 i))) (- (* (* 2.0 i) (* 2.0 i)) 1.0)))