Average Error: 62.0 → 51.5
Time: 7.2s
Precision: binary64
Cost: 576
\[lo < -1 \cdot 10^{+308} \land hi > 10^{+308}\]
\[\frac{x - lo}{hi - lo} \]
↓
\[\frac{hi}{lo} \cdot \frac{hi - x}{lo} \]
(FPCore (lo hi x) :precision binary64 (/ (- x lo) (- hi lo)))
↓
(FPCore (lo hi x) :precision binary64 (* (/ hi lo) (/ (- hi x) lo)))
double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}
↓
double code(double lo, double hi, double x) {
	return (hi / lo) * ((hi - x) / lo);
}

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) * ((hi - x) / lo)
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) * ((hi - x) / lo);
}

def code(lo, hi, x):
	return (x - lo) / (hi - lo)
↓
def code(lo, hi, x):
	return (hi / lo) * ((hi - x) / lo)

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(Float64(hi - x) / lo))
end

function tmp = code(lo, hi, x)
	tmp = (x - lo) / (hi - lo);
end
↓
function tmp = code(lo, hi, x)
	tmp = (hi / lo) * ((hi - x) / lo);
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[(N[(hi - x), $MachinePrecision] / lo), $MachinePrecision]), $MachinePrecision]

\frac{x - lo}{hi - lo}
↓
\frac{hi}{lo} \cdot \frac{hi - x}{lo}

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))))): 14 points increase in error, 11 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}{\mathsf{fma}\left(x - hi, \frac{1}{lo} \cdot \left(-1 - \frac{hi}{lo}\right), 1\right)} \]

  5. Taylor expanded in lo around 0 64.0

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

  6. Simplified51.5

    \[\leadsto \color{blue}{\frac{hi}{lo} \cdot \frac{hi - x}{lo}} \]
    Proof
    (*.f64 (/.f64 hi lo) (/.f64 (-.f64 hi x) lo)): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 hi lo) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 hi lo) (/.f64 x lo)))): 1 points increase in error, 2 points decrease in error
    (*.f64 (/.f64 hi lo) (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 hi lo) (neg.f64 (/.f64 x lo))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 hi lo) (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 hi lo)))) (neg.f64 (/.f64 x lo)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 hi lo) (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 (/.f64 hi lo)) (/.f64 x lo))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 hi lo) (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 x lo) (neg.f64 (/.f64 hi lo)))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 hi lo) (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 x lo) (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 hi lo) (neg.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 x hi) lo)))): 2 points increase in error, 1 points decrease in error
    (*.f64 (/.f64 hi lo) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 x hi) lo)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 hi lo) (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (-.f64 x hi) lo) -1))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 hi lo) (/.f64 (-.f64 x hi) lo)) -1)): 0 points increase in error, 0 points decrease in error
    (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 hi (-.f64 x hi)) (*.f64 lo lo))) -1): 256 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 x hi) hi)) (*.f64 lo lo)) -1): 0 points increase in error, 0 points decrease in error
    (*.f64 (/.f64 (*.f64 (-.f64 x hi) hi) (Rewrite<= unpow2_binary64 (pow.f64 lo 2))) -1): 0 points increase in error, 0 points decrease in error
    (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 x hi) hi) (pow.f64 lo 2)))): 0 points increase in error, 0 points decrease in error

  7. Final simplification51.5

    \[\leadsto \frac{hi}{lo} \cdot \frac{hi - x}{lo} \]

Alternatives

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

Error

Reproduce

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