xlohi (overflows)

Average Error: 62.0 → 48.5

Time: 9.4s

Precision: binary64

Cost: 1728

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

Math

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

↓

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

FPCore

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

↓

(FPCore (lo hi x)
 :precision binary64
 (+
  1.0
  (-
   (* (- (* x (/ -0.5 lo)) (- (/ x (/ lo 0.5)) (/ hi lo))) 0.5)
   (/ (- hi x) (* lo -2.0)))))

C

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

↓

double code(double lo, double hi, double x) {
	return 1.0 + ((((x * (-0.5 / lo)) - ((x / (lo / 0.5)) - (hi / lo))) * 0.5) - ((hi - x) / (lo * -2.0)));
}

Fortran

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 = 1.0d0 + ((((x * ((-0.5d0) / lo)) - ((x / (lo / 0.5d0)) - (hi / lo))) * 0.5d0) - ((hi - x) / (lo * (-2.0d0))))
end function

Java

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

Python

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

↓

def code(lo, hi, x):
	return 1.0 + ((((x * (-0.5 / lo)) - ((x / (lo / 0.5)) - (hi / lo))) * 0.5) - ((hi - x) / (lo * -2.0)))

Julia

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

↓

function code(lo, hi, x)
	return Float64(1.0 + Float64(Float64(Float64(Float64(x * Float64(-0.5 / lo)) - Float64(Float64(x / Float64(lo / 0.5)) - Float64(hi / lo))) * 0.5) - Float64(Float64(hi - x) / Float64(lo * -2.0))))
end

MATLAB

function tmp = code(lo, hi, x)
	tmp = (x - lo) / (hi - lo);
end

↓

function tmp = code(lo, hi, x)
	tmp = 1.0 + ((((x * (-0.5 / lo)) - ((x / (lo / 0.5)) - (hi / lo))) * 0.5) - ((hi - x) / (lo * -2.0)));
end

Wolfram

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

↓

code[lo_, hi_, x_] := N[(1.0 + N[(N[(N[(N[(x * N[(-0.5 / lo), $MachinePrecision]), $MachinePrecision] - N[(N[(x / N[(lo / 0.5), $MachinePrecision]), $MachinePrecision] - N[(hi / lo), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * 0.5), $MachinePrecision] - N[(N[(hi - x), $MachinePrecision] / N[(lo * -2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Derivation

1. Initial program 62.0

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

2. Taylor expanded in lo around inf 57.9

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

3. Simplified 57.9

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

   [Start] 57.9	\[ \left(-1 \cdot \frac{x}{lo} + 1\right) - -1 \cdot \frac{hi}{lo} \]
   rational.json-simplify-5 [=>] 57.9	\[ \color{blue}{-1 \cdot \frac{x}{lo} + \left(1 - -1 \cdot \frac{hi}{lo}\right)} \]
   rational.json-simplify-3 [=>] 57.9	\[ \color{blue}{1 + \left(-1 \cdot \frac{x}{lo} - -1 \cdot \frac{hi}{lo}\right)} \]
   rational.json-simplify-50 [=>] 57.9	\[ 1 + \left(\color{blue}{\frac{x}{lo} \cdot -1} - -1 \cdot \frac{hi}{lo}\right) \]
   rational.json-simplify-42 [<=] 57.9	\[ 1 + \color{blue}{-1 \cdot \left(\frac{x}{lo} - \frac{hi}{lo}\right)} \]
   rational.json-simplify-21 [<=] 57.9	\[ 1 + -1 \cdot \color{blue}{\frac{x - hi}{lo}} \]
   rational.json-simplify-41 [=>] 57.9	\[ 1 + \color{blue}{\frac{-1}{\frac{lo}{x - hi}}} \]
   rational.json-simplify-13 [=>] 57.9	\[ 1 + \color{blue}{\frac{x - hi}{\frac{lo}{-1}}} \]
   rational.json-simplify-17 [<=] 57.9	\[ 1 + \frac{x - hi}{\color{blue}{-lo}} \]

4. Applied egg-rr 48.5

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

5. Applied egg-rr 48.5

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

6. Simplified 48.5

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

   [Start] 48.5	\[ 1 + \left(\left(x \cdot \frac{-0.5}{lo} - \left(x \cdot \frac{0.5}{lo} - \frac{hi}{lo}\right)\right) \cdot 0.5 - \frac{hi - x}{lo \cdot -2}\right) \]
   rational.json-simplify-41 [=>] 48.5	\[ 1 + \left(\left(x \cdot \frac{-0.5}{lo} - \left(\color{blue}{\frac{x}{\frac{lo}{0.5}}} - \frac{hi}{lo}\right)\right) \cdot 0.5 - \frac{hi - x}{lo \cdot -2}\right) \]

7. Final simplification 48.5

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

Alternatives

Alternative 1
Error	48.5
Cost	1216

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

Alternative 2
Error	48.6
Cost	1088

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

Alternative 3
Error	48.5
Cost	1088

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

Alternative 4
Error	48.5
Cost	448

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

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 2023073 
(FPCore (lo hi x)
  :name "xlohi (overflows)"
  :precision binary64
  :pre (and (< lo -1e+308) (> hi 1e+308))
  (/ (- x lo) (- hi lo)))