xlohi (overflows)

Average Error: 62.0 → 48.6

Time: 29.9s

Precision: binary64

Cost: 2304

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

Math

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

↓

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

FPCore

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

↓

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

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

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

Python

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

↓

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

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

MATLAB

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

↓

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

Derivation

1. Initial program 62.0

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

2. Taylor expanded in lo around inf 58.0

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

3. Simplified 58.0

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

   [Start] 58.0	\[ \left(-1 \cdot \frac{x}{lo} + 1\right) - -1 \cdot \frac{hi}{lo} \]
   rational_best-simplify-21 [=>] 58.0	\[ \color{blue}{\left(-1 \cdot \frac{x}{lo} - -1\right)} - -1 \cdot \frac{hi}{lo} \]
   rational_best-simplify-48 [=>] 58.0	\[ \color{blue}{\left(-1 \cdot \frac{x}{lo} - -1 \cdot \frac{hi}{lo}\right) - -1} \]
   rational_best-simplify-20 [=>] 58.0	\[ \color{blue}{\left(-1 \cdot \frac{x}{lo} - -1 \cdot \frac{hi}{lo}\right) + 1} \]
   rational_best-simplify-1 [=>] 58.0	\[ \left(\color{blue}{\frac{x}{lo} \cdot -1} - -1 \cdot \frac{hi}{lo}\right) + 1 \]
   rational_best-simplify-62 [=>] 58.0	\[ \color{blue}{-1 \cdot \left(\frac{x}{lo} - \frac{hi}{lo}\right)} + 1 \]
   rational_best-simplify-67 [<=] 58.0	\[ -1 \cdot \color{blue}{\frac{x - hi}{lo}} + 1 \]
   rational_best-simplify-3 [=>] 58.0	\[ \color{blue}{1 + -1 \cdot \frac{x - hi}{lo}} \]
   rational_best-simplify-1 [=>] 58.0	\[ 1 + \color{blue}{\frac{x - hi}{lo} \cdot -1} \]
   rational_best-simplify-10 [=>] 58.0	\[ 1 + \color{blue}{\left(-\frac{x - hi}{lo}\right)} \]

4. Applied egg-rr 48.6

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

5. Applied egg-rr 48.6

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

6. Applied egg-rr 48.6

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

7. Simplified 48.6

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

   [Start] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \frac{\frac{hi + \left(x + \left(x - hi\right)\right)}{lo + lo}}{-2}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]
   rational_best-simplify-53 [=>] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \color{blue}{\frac{hi + \left(x + \left(x - hi\right)\right)}{\left(lo + lo\right) \cdot -2}}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]
   rational_best-simplify-1 [=>] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \frac{hi + \left(x + \left(x - hi\right)\right)}{\color{blue}{-2 \cdot \left(lo + lo\right)}}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]
   rational_best-simplify-63 [<=] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \frac{hi + \left(x + \left(x - hi\right)\right)}{\color{blue}{lo \cdot -2 + lo \cdot -2}}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]
   rational_best-simplify-1 [<=] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \frac{hi + \left(x + \left(x - hi\right)\right)}{\color{blue}{-2 \cdot lo} + lo \cdot -2}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]
   rational_best-simplify-1 [<=] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \frac{hi + \left(x + \left(x - hi\right)\right)}{-2 \cdot lo + \color{blue}{-2 \cdot lo}}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]
   rational_best-simplify-63 [=>] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \frac{hi + \left(x + \left(x - hi\right)\right)}{\color{blue}{lo \cdot \left(-2 + -2\right)}}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]
   metadata-eval [=>] 48.6	\[ 1 + \left(-\left(\frac{x}{lo} \cdot 0.5 - \left(\left(\left(0.5 \cdot \frac{hi}{lo} - \frac{x}{lo}\right) - \frac{hi + \left(x + \left(x - hi\right)\right)}{lo \cdot \color{blue}{-4}}\right) + \frac{hi}{lo + lo}\right)\right)\right) \]

8. Final simplification 48.6

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

Alternatives

Alternative 1
Error	48.6
Cost	1408

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

Alternative 2
Error	48.6
Cost	1088

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

Alternative 3
Error	48.6
Cost	768

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

Alternative 4
Error	52.0
Cost	320

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

Alternative 5
Error	52.0
Cost	256

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

Alternative 6
Error	52.1
Cost	64

\[1 \]

Reproduce

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