(/ (- x lo) (- hi lo))

Average Error: 62.0 → 1.1

Time: 13.4s

Precision: binary64

Cost: 37504

\[lo < -1 \cdot 10^{+308} \land hi > 10^{+308}\]

Math

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

↓

\[\begin{array}{l} t_0 := 1 - \frac{x}{lo}\\ t_1 := \frac{t_0}{lo \cdot \frac{lo}{hi}}\\ t_2 := {\left(hi \cdot t_1\right)}^{2}\\ t_3 := \frac{\frac{x}{lo} + -1}{lo}\\ t_0 + \frac{\left({\left(t_0 \cdot \frac{hi}{lo}\right)}^{2} - t_2\right) + \mathsf{fma}\left(hi \cdot \left(-{t_1}^{2}\right), hi, t_2\right)}{hi \cdot \left(\frac{hi}{lo} \cdot t_3\right) - hi \cdot t_3} \end{array} \]

FPCore

(FPCore (lo hi x) :precision binary64 (/ (- x lo) (- hi lo)))

↓

(FPCore (lo hi x)
 :precision binary64
 (let* ((t_0 (- 1.0 (/ x lo)))
        (t_1 (/ t_0 (* lo (/ lo hi))))
        (t_2 (pow (* hi t_1) 2.0))
        (t_3 (/ (+ (/ x lo) -1.0) lo)))
   (+
    t_0
    (/
     (+
      (- (pow (* t_0 (/ hi lo)) 2.0) t_2)
      (fma (* hi (- (pow t_1 2.0))) hi t_2))
     (- (* hi (* (/ hi lo) t_3)) (* hi t_3))))))

C

double code(double lo, double hi, double x) {
	return (x - lo) / (hi - lo);
}

↓

double code(double lo, double hi, double x) {
	double t_0 = 1.0 - (x / lo);
	double t_1 = t_0 / (lo * (lo / hi));
	double t_2 = pow((hi * t_1), 2.0);
	double t_3 = ((x / lo) + -1.0) / lo;
	return t_0 + (((pow((t_0 * (hi / lo)), 2.0) - t_2) + fma((hi * -pow(t_1, 2.0)), hi, t_2)) / ((hi * ((hi / lo) * t_3)) - (hi * t_3)));
}

Julia

function code(lo, hi, x)
	return Float64(Float64(x - lo) / Float64(hi - lo))
end

↓

function code(lo, hi, x)
	t_0 = Float64(1.0 - Float64(x / lo))
	t_1 = Float64(t_0 / Float64(lo * Float64(lo / hi)))
	t_2 = Float64(hi * t_1) ^ 2.0
	t_3 = Float64(Float64(Float64(x / lo) + -1.0) / lo)
	return Float64(t_0 + Float64(Float64(Float64((Float64(t_0 * Float64(hi / lo)) ^ 2.0) - t_2) + fma(Float64(hi * Float64(-(t_1 ^ 2.0))), hi, t_2)) / Float64(Float64(hi * Float64(Float64(hi / lo) * t_3)) - Float64(hi * t_3))))
end

Wolfram

code[lo_, hi_, x_] := N[(N[(x - lo), $MachinePrecision] / N[(hi - lo), $MachinePrecision]), $MachinePrecision]

↓

code[lo_, hi_, x_] := Block[{t$95$0 = N[(1.0 - N[(x / lo), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(t$95$0 / N[(lo * N[(lo / hi), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[Power[N[(hi * t$95$1), $MachinePrecision], 2.0], $MachinePrecision]}, Block[{t$95$3 = N[(N[(N[(x / lo), $MachinePrecision] + -1.0), $MachinePrecision] / lo), $MachinePrecision]}, N[(t$95$0 + N[(N[(N[(N[Power[N[(t$95$0 * N[(hi / lo), $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision] - t$95$2), $MachinePrecision] + N[(N[(hi * (-N[Power[t$95$1, 2.0], $MachinePrecision])), $MachinePrecision] * hi + t$95$2), $MachinePrecision]), $MachinePrecision] / N[(N[(hi * N[(N[(hi / lo), $MachinePrecision] * t$95$3), $MachinePrecision]), $MachinePrecision] - N[(hi * t$95$3), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]

Derivation

1. Initial program 62.0

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

2. Taylor expanded in hi around 0 64.0

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

3. Simplified 54.9

   \[\leadsto \color{blue}{\left(1 - \frac{x}{lo}\right) + \left(\frac{1}{lo} - \frac{x}{lo \cdot lo}\right) \cdot \left(hi + hi \cdot \frac{hi}{lo}\right)} \]
   Proof
   (+.f64 (-.f64 1 (/.f64 x lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 (/.f64 x lo)))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 1 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 x lo)))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 x lo)) 1)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (+.f64 (*.f64 -1 (/.f64 x lo)) (Rewrite<= metadata-eval (*.f64 -1 -1))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 -1 (+.f64 (/.f64 x lo) -1))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (+.f64 (/.f64 x lo) (Rewrite<= metadata-eval (neg.f64 1)))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (+.f64 (/.f64 x lo) (neg.f64 (Rewrite<= *-inverses_binary64 (/.f64 lo lo))))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 x lo) (/.f64 lo lo)))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 x lo) lo))) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (*.f64 lo lo))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 2 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (Rewrite<= unpow2_binary64 (pow.f64 lo 2)))) (+.f64 hi (*.f64 hi (/.f64 hi lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (*.f64 hi (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 hi)) lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (*.f64 hi (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 lo) hi)))))): 59 points increase in error, 64 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (*.f64 hi (Rewrite=> *-commutative_binary64 (*.f64 hi (/.f64 1 lo))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 hi hi) (/.f64 1 lo)))))): 178 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 hi 2)) (/.f64 1 lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (pow.f64 hi 2) 1) lo))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 hi hi)) 1) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 hi (*.f64 hi 1))) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (*.f64 hi (*.f64 hi (Rewrite<= metadata-eval (neg.f64 -1)))) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (*.f64 hi (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 hi -1)))) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (*.f64 hi (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 hi)))) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (*.f64 hi (neg.f64 (Rewrite=> mul-1-neg_binary64 (neg.f64 hi)))) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (*.f64 hi (Rewrite=> remove-double-neg_binary64 hi)) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) (+.f64 hi (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 hi 2)) lo)))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 hi (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2)))) (*.f64 (/.f64 (pow.f64 hi 2) lo) (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) hi)) (*.f64 (/.f64 (pow.f64 hi 2) lo) (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (*.f64 -1 (/.f64 (-.f64 x lo) lo)) (+.f64 (*.f64 (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2))) hi) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 hi 2) (-.f64 (/.f64 1 lo) (/.f64 x (pow.f64 lo 2)))) lo)))): 0 points increase in error, 0 points decrease in error

4. Applied egg-rr 51.9

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

5. Applied egg-rr 1.1

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

6. Final simplification 1.1

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

Alternatives

Alternative 1
Error	39.4
Cost	5060

\[\begin{array}{l} t_0 := 1 - \frac{x}{lo}\\ t_1 := \frac{\frac{x}{lo} + -1}{lo}\\ t_2 := hi \cdot t_1\\ \mathbf{if}\;lo \leq -1.444 \cdot 10^{+308}:\\ \;\;\;\;t_0 - \frac{\frac{\left(t_0 \cdot \frac{hi}{lo}\right) \cdot \left(hi \cdot \left(hi \cdot \frac{t_0}{lo \cdot \frac{lo}{hi}}\right)\right)}{lo} + \left(hi \cdot \frac{t_0}{lo}\right) \cdot t_2}{hi \cdot \left(\frac{hi}{lo} \cdot t_1\right) - t_2}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{hi} + lo \cdot \left(\frac{-1}{hi} - \frac{x}{hi} \cdot \frac{1}{hi}\right)\\ \end{array} \]

Alternative 2
Error	1.1
Cost	4928

\[\begin{array}{l} t_0 := 1 - \frac{x}{lo}\\ t_1 := \frac{\frac{x}{lo} + -1}{lo}\\ t_2 := hi \cdot \left(\frac{hi}{lo} \cdot t_1\right)\\ t_3 := hi \cdot t_1\\ t_0 + \frac{t_3 \cdot t_3 + \left(hi \cdot \frac{hi}{\frac{lo \cdot lo}{t_0}}\right) \cdot t_2}{t_2 - t_3} \end{array} \]

Alternative 3
Error	51.5
Cost	4800

\[\begin{array}{l} t_0 := \frac{\frac{x}{lo} + -1}{lo}\\ t_1 := hi \cdot \left(\frac{hi}{lo} \cdot t_0\right)\\ t_2 := hi \cdot t_0\\ \left(1 - \frac{x}{lo}\right) + \frac{t_2 \cdot t_2 - t_1 \cdot t_1}{t_1 - \frac{x}{lo} \cdot \frac{hi}{lo}} \end{array} \]

Alternative 4
Error	51.9
Cost	1344

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

Alternative 5
Error	52.0
Cost	320

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

Alternative 6
Error	52.0
Cost	256

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

Alternative 7
Error	52.0
Cost	64

\[1 \]

Reproduce

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