Average Error: 62.0 → 51.6
Time: 6.7s
Precision: binary64
Cost: 448
\[lo < -1 \cdot 10^{+308} \land hi > 10^{+308}\]
\[\frac{x - lo}{hi - lo} \]
\[\frac{\frac{hi}{lo}}{\frac{lo}{hi}} \]
(FPCore (lo hi x) :precision binary64 (/ (- x lo) (- hi lo)))
(FPCore (lo hi x) :precision binary64 (/ (/ hi lo) (/ lo hi)))
double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}
double code(double lo, double hi, double x) {
	return (hi / lo) / (lo / hi);
}
real(8) function code(lo, hi, x)
    real(8), intent (in) :: lo
    real(8), intent (in) :: hi
    real(8), intent (in) :: x
    code = (x - lo) / (hi - lo)
end function
real(8) function code(lo, hi, x)
    real(8), intent (in) :: lo
    real(8), intent (in) :: hi
    real(8), intent (in) :: x
    code = (hi / lo) / (lo / hi)
end function
public static double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}
public static double code(double lo, double hi, double x) {
	return (hi / lo) / (lo / hi);
}
def code(lo, hi, x):
	return (x - lo) / (hi - lo)
def code(lo, hi, x):
	return (hi / lo) / (lo / hi)
function code(lo, hi, x)
	return Float64(Float64(x - lo) / Float64(hi - lo))
end
function code(lo, hi, x)
	return Float64(Float64(hi / lo) / Float64(lo / hi))
end
function tmp = code(lo, hi, x)
	tmp = (x - lo) / (hi - lo);
end
function tmp = code(lo, hi, x)
	tmp = (hi / lo) / (lo / hi);
end
code[lo_, hi_, x_] := N[(N[(x - lo), $MachinePrecision] / N[(hi - lo), $MachinePrecision]), $MachinePrecision]
code[lo_, hi_, x_] := N[(N[(hi / lo), $MachinePrecision] / N[(lo / hi), $MachinePrecision]), $MachinePrecision]
\frac{x - lo}{hi - lo}
\frac{\frac{hi}{lo}}{\frac{lo}{hi}}

Error

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 62.0

    \[\frac{x - lo}{hi - lo} \]
  2. Taylor expanded in lo around inf 64.0

    \[\leadsto \color{blue}{\left(-1 \cdot \frac{x}{lo} + \left(\frac{hi \cdot \left(-1 \cdot x - -1 \cdot hi\right)}{{lo}^{2}} + 1\right)\right) - -1 \cdot \frac{hi}{lo}} \]
  3. Simplified51.9

    \[\leadsto \color{blue}{1 + \frac{x - hi}{lo} \cdot \left(-1 - \frac{hi}{lo}\right)} \]
    Proof
    (+.f64 1 (*.f64 (/.f64 (-.f64 x hi) lo) (-.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (*.f64 (/.f64 hi lo) (/.f64 (-.f64 x hi) lo))))): 11 points increase in error, 19 points decrease in error
    (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi (-.f64 x hi)) (*.f64 lo lo))))): 256 points increase in error, 0 points decrease in error
    (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 x hi) hi)) (*.f64 lo lo)))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (-.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (/.f64 (*.f64 (-.f64 x hi) hi) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (neg.f64 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (+.f64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))))): 0 points increase in error, 0 points decrease in error
    (+.f64 1 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 1 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))) (*.f64 -1 (/.f64 (-.f64 x hi) lo)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (*.f64 (-.f64 x hi) hi)) (pow.f64 lo 2)))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 -1 (-.f64 x hi)) hi)) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (/.f64 (*.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) hi) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi)))) (pow.f64 lo 2))) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1)) (*.f64 -1 (/.f64 (-.f64 x hi) lo))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 x lo) (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 x lo)) (*.f64 -1 (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1) (*.f64 -1 (/.f64 x lo))) (*.f64 -1 (/.f64 hi lo)))): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 x lo)) (+.f64 (/.f64 (*.f64 hi (-.f64 (*.f64 -1 x) (*.f64 -1 hi))) (pow.f64 lo 2)) 1))) (*.f64 -1 (/.f64 hi lo))): 0 points increase in error, 0 points decrease in error
  4. Applied egg-rr51.9

    \[\leadsto \color{blue}{\sqrt[3]{{\left(\mathsf{fma}\left(-1 - \frac{hi}{lo}, \frac{x - hi}{lo}, 1\right)\right)}^{3}}} \]
  5. Taylor expanded in hi around inf 64.0

    \[\leadsto \color{blue}{\frac{{hi}^{2}}{{lo}^{2}}} \]
  6. Simplified51.6

    \[\leadsto \color{blue}{\frac{hi}{lo} \cdot \frac{hi}{lo}} \]
    Proof
    (*.f64 (/.f64 hi lo) (/.f64 hi lo)): 0 points increase in error, 0 points decrease in error
    (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi hi) (*.f64 lo lo))): 256 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 hi 2)) (*.f64 lo lo)): 0 points increase in error, 0 points decrease in error
    (/.f64 (pow.f64 hi 2) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))): 0 points increase in error, 0 points decrease in error
  7. Applied egg-rr51.6

    \[\leadsto \color{blue}{\frac{\frac{hi}{lo}}{\frac{lo}{hi}}} \]
  8. Final simplification51.6

    \[\leadsto \frac{\frac{hi}{lo}}{\frac{lo}{hi}} \]

Alternatives

Alternative 1
Error52.0
Cost256
\[\frac{-lo}{hi} \]
Alternative 2
Error52.1
Cost64
\[1 \]

Error

Reproduce

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