Average Error: 2.4 → 0.5
Time: 24.9s
Precision: 64
Internal Precision: 320
\[\frac{\frac{\left(i \cdot i\right) \cdot \left(i \cdot i\right)}{\left(2 \cdot i\right) \cdot \left(2 \cdot i\right)}}{\left(2 \cdot i\right) \cdot \left(2 \cdot i\right) - 1.0}\]
↓
\[\frac{i}{2 \cdot \left(1.0 + i \cdot 2\right)} \cdot \frac{i}{\left(i \cdot 2 - 1.0\right) \cdot 2}\]

Error

Bits error versus i

Derivation

  1. Initial program 2.4

    \[\frac{\left(\frac{\left(\left(i \cdot i\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(\left(real->posit(2)\right) \cdot i\right) \cdot \left(\left(real->posit(2)\right) \cdot i\right)\right)}\right)}{\left(\left(\left(\left(real->posit(2)\right) \cdot i\right) \cdot \left(\left(real->posit(2)\right) \cdot i\right)\right) - \left(real->posit(1.0)\right)\right)}\]
  2. Using strategy rm

  3. Applied p16-times-frac1.1

    \[\leadsto \frac{\color{blue}{\left(\left(\frac{\left(i \cdot i\right)}{\left(\left(real->posit(2)\right) \cdot i\right)}\right) \cdot \left(\frac{\left(i \cdot i\right)}{\left(\left(real->posit(2)\right) \cdot i\right)}\right)\right)}}{\left(\left(\left(\left(real->posit(2)\right) \cdot i\right) \cdot \left(\left(real->posit(2)\right) \cdot i\right)\right) - \left(real->posit(1.0)\right)\right)}\]
  4. Using strategy rm

  5. Applied p16-times-frac0.9

    \[\leadsto \frac{\left(\color{blue}{\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(\frac{i}{i}\right)\right)} \cdot \left(\frac{\left(i \cdot i\right)}{\left(\left(real->posit(2)\right) \cdot i\right)}\right)\right)}{\left(\left(\left(\left(real->posit(2)\right) \cdot i\right) \cdot \left(\left(real->posit(2)\right) \cdot i\right)\right) - \left(real->posit(1.0)\right)\right)}\]

  6. Simplified0.9

    \[\leadsto \frac{\left(\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \color{blue}{\left(real->posit(1.0)\right)}\right) \cdot \left(\frac{\left(i \cdot i\right)}{\left(\left(real->posit(2)\right) \cdot i\right)}\right)\right)}{\left(\left(\left(\left(real->posit(2)\right) \cdot i\right) \cdot \left(\left(real->posit(2)\right) \cdot i\right)\right) - \left(real->posit(1.0)\right)\right)}\]
  7. Using strategy rm

  8. Applied difference-of-sqr-10.8

    \[\leadsto \frac{\left(\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right) \cdot \left(\frac{\left(i \cdot i\right)}{\left(\left(real->posit(2)\right) \cdot i\right)}\right)\right)}{\color{blue}{\left(\left(\frac{\left(\left(real->posit(2)\right) \cdot i\right)}{\left(real->posit(1.0)\right)}\right) \cdot \left(\left(\left(real->posit(2)\right) \cdot i\right) - \left(real->posit(1.0)\right)\right)\right)}}\]

  9. Applied p16-times-frac0.8

    \[\leadsto \color{blue}{\left(\frac{\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right)}{\left(\frac{\left(\left(real->posit(2)\right) \cdot i\right)}{\left(real->posit(1.0)\right)}\right)}\right) \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(real->posit(2)\right) \cdot i\right)}\right)}{\left(\left(\left(real->posit(2)\right) \cdot i\right) - \left(real->posit(1.0)\right)\right)}\right)}\]

  10. Simplified0.8

    \[\leadsto \color{blue}{\left(\frac{i}{\left(\left(real->posit(2)\right) \cdot \left(\frac{\left(real->posit(1.0)\right)}{\left(i \cdot \left(real->posit(2)\right)\right)}\right)\right)}\right)} \cdot \left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(real->posit(2)\right) \cdot i\right)}\right)}{\left(\left(\left(real->posit(2)\right) \cdot i\right) - \left(real->posit(1.0)\right)\right)}\right)\]

  11. Simplified0.5

    \[\leadsto \left(\frac{i}{\left(\left(real->posit(2)\right) \cdot \left(\frac{\left(real->posit(1.0)\right)}{\left(i \cdot \left(real->posit(2)\right)\right)}\right)\right)}\right) \cdot \color{blue}{\left(\frac{i}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right) \cdot \left(real->posit(2)\right)\right)}\right)}\]

  12. Final simplification0.5

    \[\leadsto \frac{i}{2 \cdot \left(1.0 + i \cdot 2\right)} \cdot \frac{i}{\left(i \cdot 2 - 1.0\right) \cdot 2}\]

Reproduce

herbie shell --seed 2019068 
(FPCore (i)
  :name "Octave 3.8, jcobi/4, as called"
  :pre (and (>.p16 i (real->posit16 0)))
  (/.p16 (/.p16 (*.p16 (*.p16 i i) (*.p16 i i)) (*.p16 (*.p16 (real->posit16 2) i) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (*.p16 (real->posit16 2) i) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))