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

Average Error: 62.0 → 51.2

Time: 11.2s

Precision: binary64

Cost: 24768

\[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 := \frac{t_0}{lo}\\ t_3 := hi \cdot t_2\\ t_0 + \frac{{t_3}^{3} + {\left(hi \cdot \left(t_2 \cdot \frac{hi}{lo}\right)\right)}^{3}}{\mathsf{fma}\left(t_3, t_3, t_1 \cdot \left(hi \cdot \left(hi \cdot t_1 - t_0 \cdot \frac{hi}{lo}\right)\right)\right)} \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 (/ t_0 lo))
        (t_3 (* hi t_2)))
   (+
    t_0
    (/
     (+ (pow t_3 3.0) (pow (* hi (* t_2 (/ hi lo))) 3.0))
     (fma t_3 t_3 (* t_1 (* hi (- (* hi t_1) (* t_0 (/ hi lo))))))))))

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 = t_0 / lo;
	double t_3 = hi * t_2;
	return t_0 + ((pow(t_3, 3.0) + pow((hi * (t_2 * (hi / lo))), 3.0)) / fma(t_3, t_3, (t_1 * (hi * ((hi * t_1) - (t_0 * (hi / lo)))))));
}

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(t_0 / lo)
	t_3 = Float64(hi * t_2)
	return Float64(t_0 + Float64(Float64((t_3 ^ 3.0) + (Float64(hi * Float64(t_2 * Float64(hi / lo))) ^ 3.0)) / fma(t_3, t_3, Float64(t_1 * Float64(hi * Float64(Float64(hi * t_1) - Float64(t_0 * Float64(hi / lo))))))))
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[(t$95$0 / lo), $MachinePrecision]}, Block[{t$95$3 = N[(hi * t$95$2), $MachinePrecision]}, N[(t$95$0 + N[(N[(N[Power[t$95$3, 3.0], $MachinePrecision] + N[Power[N[(hi * N[(t$95$2 * N[(hi / lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 3.0], $MachinePrecision]), $MachinePrecision] / N[(t$95$3 * t$95$3 + N[(t$95$1 * N[(hi * N[(N[(hi * t$95$1), $MachinePrecision] - N[(t$95$0 * N[(hi / lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $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))))): 1 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)))))): 65 points increase in error, 74 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)))))): 187 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)}^{3} + {\left(hi \cdot \left(\frac{hi}{lo} \cdot \frac{1 - \frac{x}{lo}}{lo}\right)\right)}^{3}}{\mathsf{fma}\left(hi \cdot \frac{1 - \frac{x}{lo}}{lo}, hi \cdot \frac{1 - \frac{x}{lo}}{lo}, \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) - \left(hi \cdot \frac{1 - \frac{x}{lo}}{lo}\right) \cdot \left(hi \cdot \left(\frac{hi}{lo} \cdot \frac{1 - \frac{x}{lo}}{lo}\right)\right)\right)}} \]

5. Applied egg-rr 51.6

   \[\leadsto \left(1 - \frac{x}{lo}\right) + \frac{{\left(hi \cdot \frac{1 - \frac{x}{lo}}{lo}\right)}^{3} + {\left(hi \cdot \left(\frac{hi}{lo} \cdot \frac{1 - \frac{x}{lo}}{lo}\right)\right)}^{3}}{\mathsf{fma}\left(hi \cdot \frac{1 - \frac{x}{lo}}{lo}, hi \cdot \frac{1 - \frac{x}{lo}}{lo}, \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) - \color{blue}{\sqrt{{\left(\left(1 - \frac{x}{lo}\right) \cdot \frac{hi}{lo}\right)}^{2}}} \cdot \left(hi \cdot \left(\frac{hi}{lo} \cdot \frac{1 - \frac{x}{lo}}{lo}\right)\right)\right)} \]

6. Applied egg-rr 51.2

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

7. Final simplification 51.2

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

Alternatives

Alternative 1
Error	51.7
Cost	13440

\[\sqrt{{\left(\frac{lo}{hi}\right)}^{2}} \cdot \frac{x - lo}{hi} \]

Alternative 2
Error	51.9
Cost	1728

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

Alternative 3
Error	51.9
Cost	1472

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

Alternative 4
Error	51.9
Cost	704

\[1 + hi \cdot \frac{1 + \frac{hi}{lo}}{lo} \]

Alternative 5
Error	51.9
Cost	704

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

Alternative 6
Error	52.0
Cost	320

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

Alternative 7
Error	52.0
Cost	256

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

Alternative 8
Error	52.0
Cost	64

\[1 \]

Reproduce

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