xlohi (overflows)

Average Error: 62.0 → 0.3

Time: 8.7s

Precision: binary64

Cost: 832

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

Math

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

↓

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

FPCore

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

↓

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

C

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

↓

double code(double lo, double hi, double x) {
	return ((lo / hi) - (x / hi)) / ((lo / hi) + -1.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 = ((lo / hi) - (x / hi)) / ((lo / hi) + (-1.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 ((lo / hi) - (x / hi)) / ((lo / hi) + -1.0);
}

Python

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

↓

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

Julia

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

↓

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

MATLAB

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

↓

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

Wolfram

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

↓

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

Derivation

1. Initial program 62.0

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

2. Taylor expanded in hi around inf 64.0

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

3. Simplified 57.9

   \[\leadsto \color{blue}{\frac{x - lo}{hi} \cdot \frac{lo}{hi} + \frac{x - lo}{hi}} \]
   Proof
   (+.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) (/.f64 (-.f64 x lo) hi)): 0 points increase in error, 0 points decrease in error
   (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 x lo) lo) (*.f64 hi hi))) (/.f64 (-.f64 x lo) hi)): 255 points increase in error, 0 points decrease in error
   (+.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 lo (-.f64 x lo))) (*.f64 hi hi)) (/.f64 (-.f64 x lo) hi)): 0 points increase in error, 0 points decrease in error
   (+.f64 (/.f64 (*.f64 lo (-.f64 x lo)) (Rewrite<= unpow2_binary64 (pow.f64 hi 2))) (/.f64 (-.f64 x lo) hi)): 0 points increase in error, 0 points decrease in error
   (+.f64 (/.f64 (*.f64 lo (-.f64 x lo)) (pow.f64 hi 2)) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 x hi) (/.f64 lo hi)))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (*.f64 lo (-.f64 x lo)) (pow.f64 hi 2)) (/.f64 x hi)) (/.f64 lo hi))): 0 points increase in error, 0 points decrease in error
   (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 x hi) (/.f64 (*.f64 lo (-.f64 x lo)) (pow.f64 hi 2)))) (/.f64 lo hi)): 0 points increase in error, 0 points decrease in error

4. Applied egg-rr 57.9

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

5. Simplified 0.4

   \[\leadsto \color{blue}{\frac{\frac{{\left(lo \cdot \frac{x - lo}{hi \cdot hi}\right)}^{2}}{\frac{x - lo}{hi}} - \frac{x - lo}{hi}}{-1 + \frac{lo}{hi}}} \]
   Proof
   (/.f64 (-.f64 (/.f64 (pow.f64 (*.f64 lo (/.f64 (-.f64 x lo) (*.f64 hi hi))) 2) (/.f64 (-.f64 x lo) hi)) (/.f64 (-.f64 x lo) hi)) (+.f64 -1 (/.f64 lo hi))): 0 points increase in error, 0 points decrease in error
   (/.f64 (-.f64 (/.f64 (pow.f64 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (-.f64 x lo) (*.f64 hi hi)) lo)) 2) (/.f64 (-.f64 x lo) hi)) (/.f64 (-.f64 x lo) hi)) (+.f64 -1 (/.f64 lo hi))): 0 points increase in error, 0 points decrease in error
   (/.f64 (-.f64 (/.f64 (pow.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 x lo) lo) (*.f64 hi hi))) 2) (/.f64 (-.f64 x lo) hi)) (/.f64 (-.f64 x lo) hi)) (+.f64 -1 (/.f64 lo hi))): 255 points increase in error, 0 points decrease in error
   (/.f64 (-.f64 (/.f64 (pow.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi))) 2) (/.f64 (-.f64 x lo) hi)) (/.f64 (-.f64 x lo) hi)) (+.f64 -1 (/.f64 lo hi))): 0 points increase in error, 255 points decrease in error
   (/.f64 (-.f64 (/.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (/.f64 (-.f64 x lo) hi)) (Rewrite<= /-rgt-identity_binary64 (/.f64 (/.f64 (-.f64 x lo) hi) 1))) (+.f64 -1 (/.f64 lo hi))): 0 points increase in error, 0 points decrease in error
   (/.f64 (-.f64 (/.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (/.f64 (-.f64 x lo) hi)) (/.f64 (/.f64 (-.f64 x lo) hi) (Rewrite<= *-inverses_binary64 (/.f64 (/.f64 (-.f64 x lo) hi) (/.f64 (-.f64 x lo) hi))))) (+.f64 -1 (/.f64 lo hi))): 0 points increase in error, 0 points decrease in error
   (/.f64 (-.f64 (/.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (/.f64 (-.f64 x lo) hi)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 (-.f64 x lo) hi)) (/.f64 (-.f64 x lo) hi)))) (+.f64 -1 (/.f64 lo hi))): 4 points increase in error, 9 points decrease in error
   (/.f64 (-.f64 (/.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (/.f64 (-.f64 x lo) hi)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2)) (/.f64 (-.f64 x lo) hi))) (+.f64 -1 (/.f64 lo hi))): 0 points increase in error, 0 points decrease in error
   (/.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)) (/.f64 (-.f64 x lo) hi))) (+.f64 -1 (/.f64 lo hi))): 102 points increase in error, 82 points decrease in error
   (/.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)) (/.f64 (-.f64 x lo) hi)) (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 lo hi) -1))): 0 points increase in error, 0 points decrease in error
   (/.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)) (/.f64 (-.f64 x lo) hi)) (+.f64 (/.f64 lo hi) (Rewrite<= metadata-eval (neg.f64 1)))): 0 points increase in error, 0 points decrease in error
   (/.f64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)) (/.f64 (-.f64 x lo) hi)) (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 lo hi) 1))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (pow.f64 (/.f64 (-.f64 x lo) hi) 2)) (*.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 lo hi) 1)))): 44 points increase in error, 55 points decrease in error
   (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (pow.f64 (*.f64 (/.f64 (-.f64 x lo) hi) (/.f64 lo hi)) 2) (*.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 lo hi) 1))) (/.f64 (pow.f64 (/.f64 (-.f64 x lo) hi) 2) (*.f64 (/.f64 (-.f64 x lo) hi) (-.f64 (/.f64 lo hi) 1))))): 85 points increase in error, 94 points decrease in error

6. Taylor expanded in lo around 0 0.3

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

7. Simplified 0.3

   \[\leadsto \frac{\color{blue}{\frac{lo}{hi} + \left(-\frac{x}{hi}\right)}}{-1 + \frac{lo}{hi}} \]
   Proof
   (+.f64 (/.f64 lo hi) (neg.f64 (/.f64 x hi))): 0 points increase in error, 0 points decrease in error
   (+.f64 (/.f64 lo hi) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 x hi)))): 0 points increase in error, 0 points decrease in error

8. Applied egg-rr 0.3

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

9. Final simplification 0.3

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

Alternatives

Alternative 1
Error	0.4
Cost	704

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

Alternative 2
Error	1.0
Cost	576

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

Alternative 3
Error	52.0
Cost	256

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

Alternative 4
Error	52.1
Cost	64

\[1 \]

Reproduce

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