xlohi (overflows)

Average Error: 62.0 → 48.5

Time: 19.1s

Precision: binary64

Cost: 1152

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

Math

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

↓

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

FPCore

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

↓

(FPCore (lo hi x)
 :precision binary64
 (- (* (- x lo) (+ (/ 0.5 lo) (/ 1.0 (* lo (/ (+ lo 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 -((x - lo) * ((0.5 / lo) + (1.0 / (lo * ((lo + 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 = -((x - lo) * ((0.5d0 / lo) + (1.0d0 / (lo * ((lo + 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 -((x - lo) * ((0.5 / lo) + (1.0 / (lo * ((lo + lo) / lo)))));
}

Python

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

↓

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

Julia

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

↓

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

MATLAB

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

↓

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

Wolfram

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

↓

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

Derivation

1. Initial program 62.0

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

2. Taylor expanded in hi around 0 52.0

   \[\leadsto \color{blue}{-1 \cdot \frac{x - lo}{lo}} \]

3. Simplified 52.0

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

   [Start] 52.0	\[ -1 \cdot \frac{x - lo}{lo} \]
   rational.json-simplify-2 [=>] 52.0	\[ \color{blue}{\frac{x - lo}{lo} \cdot -1} \]
   rational.json-simplify-9 [=>] 52.0	\[ \color{blue}{-\frac{x - lo}{lo}} \]

4. Applied egg-rr 52.0

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

5. Simplified 52.0

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

   [Start] 52.0	\[ -\left(\left(x - lo\right) \cdot \frac{0.5}{lo} + \left(x - lo\right) \cdot \frac{0.5}{lo}\right) \]
   rational.json-simplify-2 [=>] 52.0	\[ -\left(\color{blue}{\frac{0.5}{lo} \cdot \left(x - lo\right)} + \left(x - lo\right) \cdot \frac{0.5}{lo}\right) \]
   rational.json-simplify-51 [=>] 64.0	\[ -\color{blue}{\frac{0.5}{lo} \cdot \left(\left(x - lo\right) + \left(x - lo\right)\right)} \]
   rational.json-simplify-7 [<=] 64.0	\[ -\frac{0.5}{lo} \cdot \left(\left(x - lo\right) + \color{blue}{\frac{x - lo}{1}}\right) \]
   rational.json-simplify-30 [<=] 64.0	\[ -\frac{0.5}{lo} \cdot \color{blue}{\left(\left(1 + 1\right) \cdot \frac{x - lo}{1}\right)} \]
   metadata-eval [=>] 64.0	\[ -\frac{0.5}{lo} \cdot \left(\color{blue}{2} \cdot \frac{x - lo}{1}\right) \]
   rational.json-simplify-7 [=>] 64.0	\[ -\frac{0.5}{lo} \cdot \left(2 \cdot \color{blue}{\left(x - lo\right)}\right) \]
   rational.json-simplify-43 [<=] 52.0	\[ -\color{blue}{\left(x - lo\right) \cdot \left(\frac{0.5}{lo} \cdot 2\right)} \]

6. Applied egg-rr 64.0

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

7. Simplified 48.5

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

   [Start] 64.0	\[ -\left(x - lo\right) \cdot \frac{\left(lo + lo\right) + \frac{lo \cdot \left(lo \cdot 4\right)}{lo + lo}}{\left(lo + lo\right) \cdot \frac{lo \cdot \left(lo \cdot 4\right)}{lo + lo}} \]
   rational.json-simplify-28 [=>] 64.0	\[ -\left(x - lo\right) \cdot \color{blue}{\left(\frac{1}{lo + lo} + \frac{1}{\frac{lo \cdot \left(lo \cdot 4\right)}{lo + lo}}\right)} \]
   metadata-eval [<=] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{\color{blue}{0.5 + 0.5}}{lo + lo} + \frac{1}{\frac{lo \cdot \left(lo \cdot 4\right)}{lo + lo}}\right) \]
   rational.json-simplify-35 [<=] 64.0	\[ -\left(x - lo\right) \cdot \left(\color{blue}{\frac{0.5}{lo}} + \frac{1}{\frac{lo \cdot \left(lo \cdot 4\right)}{lo + lo}}\right) \]
   rational.json-simplify-2 [=>] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{\frac{\color{blue}{\left(lo \cdot 4\right) \cdot lo}}{lo + lo}}\right) \]
   rational.json-simplify-49 [=>] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{\color{blue}{lo \cdot \frac{lo \cdot 4}{lo + lo}}}\right) \]
   metadata-eval [<=] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{lo \cdot \color{blue}{\left(2 + 2\right)}}{lo + lo}}\right) \]
   rational.json-simplify-51 [<=] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{\color{blue}{lo \cdot 2 + 2 \cdot lo}}{lo + lo}}\right) \]
   rational.json-simplify-2 [<=] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{lo \cdot 2 + \color{blue}{lo \cdot 2}}{lo + lo}}\right) \]
   rational.json-simplify-2 [=>] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{\color{blue}{2 \cdot lo} + lo \cdot 2}{lo + lo}}\right) \]
   rational.json-simplify-51 [=>] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{\color{blue}{2 \cdot \left(lo + lo\right)}}{lo + lo}}\right) \]
   metadata-eval [<=] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{\color{blue}{\left(1 + 1\right)} \cdot \left(lo + lo\right)}{lo + lo}}\right) \]
   rational.json-simplify-7 [<=] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{\left(1 + 1\right) \cdot \color{blue}{\frac{lo + lo}{1}}}{lo + lo}}\right) \]
   rational.json-simplify-30 [=>] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{\color{blue}{\left(lo + lo\right) + \frac{lo + lo}{1}}}{lo + lo}}\right) \]
   rational.json-simplify-7 [=>] 64.0	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \frac{\left(lo + lo\right) + \color{blue}{\left(lo + lo\right)}}{lo + lo}}\right) \]
   rational.json-simplify-35 [<=] 48.5	\[ -\left(x - lo\right) \cdot \left(\frac{0.5}{lo} + \frac{1}{lo \cdot \color{blue}{\frac{lo + lo}{lo}}}\right) \]

8. Final simplification 48.5

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

Alternatives

Alternative 1
Error	52.0
Cost	256

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

Alternative 2
Error	52.1
Cost	64

\[1 \]

Reproduce

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