Average Error: 62.0 → 1.0
Time: 10.9s
Precision: 64
\[lo \lt -1.000000000000000010979063629440455417405 \cdot 10^{308} \land hi \gt 1.000000000000000010979063629440455417405 \cdot 10^{308}\]
\[\frac{x - lo}{hi - lo}\]
↓
\[\frac{x}{hi - lo} - \frac{\frac{hi}{lo} + 1}{\mathsf{fma}\left(\frac{hi}{lo}, \frac{hi}{lo}, -1\right)}\]
\frac{x - lo}{hi - lo}
↓
\frac{x}{hi - lo} - \frac{\frac{hi}{lo} + 1}{\mathsf{fma}\left(\frac{hi}{lo}, \frac{hi}{lo}, -1\right)}
double f(double lo, double hi, double x) {
        double r26900 = x;
        double r26901 = lo;
        double r26902 = r26900 - r26901;
        double r26903 = hi;
        double r26904 = r26903 - r26901;
        double r26905 = r26902 / r26904;
        return r26905;
}
↓
double f(double lo, double hi, double x) {
        double r26906 = x;
        double r26907 = hi;
        double r26908 = lo;
        double r26909 = r26907 - r26908;
        double r26910 = r26906 / r26909;
        double r26911 = r26907 / r26908;
        double r26912 = 1.0;
        double r26913 = r26911 + r26912;
        double r26914 = -1.0;
        double r26915 = fma(r26911, r26911, r26914);
        double r26916 = r26913 / r26915;
        double r26917 = r26910 - r26916;
        return r26917;
}

Error

Bits error versus lo

Bits error versus hi

Bits error versus x

Derivation

  1. Initial program 62.0

    \[\frac{x - lo}{hi - lo}\]
  2. Using strategy rm

  3. Applied div-sub62.0

    \[\leadsto \color{blue}{\frac{x}{hi - lo} - \frac{lo}{hi - lo}}\]
  4. Using strategy rm

  5. Applied clear-num62.0

    \[\leadsto \frac{x}{hi - lo} - \color{blue}{\frac{1}{\frac{hi - lo}{lo}}}\]

  6. Simplified1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\color{blue}{\frac{hi}{lo} - 1}}\]
  7. Using strategy rm

  8. Applied flip--1.8

    \[\leadsto \frac{x}{hi - lo} - \frac{1}{\color{blue}{\frac{\frac{hi}{lo} \cdot \frac{hi}{lo} - 1 \cdot 1}{\frac{hi}{lo} + 1}}}\]

  9. Applied associate-/r/1.8

    \[\leadsto \frac{x}{hi - lo} - \color{blue}{\frac{1}{\frac{hi}{lo} \cdot \frac{hi}{lo} - 1 \cdot 1} \cdot \left(\frac{hi}{lo} + 1\right)}\]

  10. Simplified1.1

    \[\leadsto \frac{x}{hi - lo} - \color{blue}{\frac{1}{\mathsf{fma}\left(\frac{hi}{lo}, \frac{hi}{lo}, -1\right)}} \cdot \left(\frac{hi}{lo} + 1\right)\]
  11. Using strategy rm

  12. Applied associate-*l/1.0

    \[\leadsto \frac{x}{hi - lo} - \color{blue}{\frac{1 \cdot \left(\frac{hi}{lo} + 1\right)}{\mathsf{fma}\left(\frac{hi}{lo}, \frac{hi}{lo}, -1\right)}}\]

  13. Simplified1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{\color{blue}{\frac{hi}{lo} + 1}}{\mathsf{fma}\left(\frac{hi}{lo}, \frac{hi}{lo}, -1\right)}\]

  14. Final simplification1.0

    \[\leadsto \frac{x}{hi - lo} - \frac{\frac{hi}{lo} + 1}{\mathsf{fma}\left(\frac{hi}{lo}, \frac{hi}{lo}, -1\right)}\]

Reproduce

herbie shell --seed 2019351 +o rules:numerics
(FPCore (lo hi x)
  :name "(/ (- x lo) (- hi lo))"
  :precision binary64
  :pre (and (< lo -1e+308) (> hi 1e+308))
  (/ (- x lo) (- hi lo)))