xlohi (overflows)

Average Accuracy: 3.1% → 98.6%

Time: 10.2s

Precision: binary64

Cost: 13184

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

Math

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

↓

\[e^{-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)} \]

FPCore

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

↓

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

C

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

↓

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

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 Math.exp(-Math.log1p(((x - hi) / lo)));
}

Python

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

↓

def code(lo, hi, x):
	return math.exp(-math.log1p(((x - hi) / lo)))

Julia

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

↓

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

Wolfram

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

↓

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

Derivation

1. Initial program 3.1%

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

2. Taylor expanded in lo around inf 9.7%

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

3. Simplified 9.6%

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

   [Start] 9.7	\[ \left(-1 \cdot \frac{x}{lo} + 1\right) - -1 \cdot \frac{hi}{lo} \]
   +-commutative [=>] 9.7	\[ \color{blue}{\left(1 + -1 \cdot \frac{x}{lo}\right)} - -1 \cdot \frac{hi}{lo} \]
   associate--l+ [=>] 9.7	\[ \color{blue}{1 + \left(-1 \cdot \frac{x}{lo} - -1 \cdot \frac{hi}{lo}\right)} \]
   associate-*r/ [=>] 9.7	\[ 1 + \left(\color{blue}{\frac{-1 \cdot x}{lo}} - -1 \cdot \frac{hi}{lo}\right) \]
   associate-*r/ [=>] 9.7	\[ 1 + \left(\frac{-1 \cdot x}{lo} - \color{blue}{\frac{-1 \cdot hi}{lo}}\right) \]
   div-sub [<=] 9.6	\[ 1 + \color{blue}{\frac{-1 \cdot x - -1 \cdot hi}{lo}} \]
   distribute-lft-out-- [=>] 9.6	\[ 1 + \frac{\color{blue}{-1 \cdot \left(x - hi\right)}}{lo} \]
   associate-*r/ [<=] 9.6	\[ 1 + \color{blue}{-1 \cdot \frac{x - hi}{lo}} \]
   mul-1-neg [=>] 9.6	\[ 1 + \color{blue}{\left(-\frac{x - hi}{lo}\right)} \]
   unsub-neg [=>] 9.6	\[ \color{blue}{1 - \frac{x - hi}{lo}} \]

4. Applied egg-rr 9.6%

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

   [Start] 9.6	\[ 1 - \frac{x - hi}{lo} \]
   flip-- [=>] 9.6	\[ \color{blue}{\frac{1 \cdot 1 - \frac{x - hi}{lo} \cdot \frac{x - hi}{lo}}{1 + \frac{x - hi}{lo}}} \]
   div-inv [=>] 9.6	\[ \color{blue}{\left(1 \cdot 1 - \frac{x - hi}{lo} \cdot \frac{x - hi}{lo}\right) \cdot \frac{1}{1 + \frac{x - hi}{lo}}} \]
   metadata-eval [=>] 9.6	\[ \left(\color{blue}{1} - \frac{x - hi}{lo} \cdot \frac{x - hi}{lo}\right) \cdot \frac{1}{1 + \frac{x - hi}{lo}} \]
   pow2 [=>] 9.6	\[ \left(1 - \color{blue}{{\left(\frac{x - hi}{lo}\right)}^{2}}\right) \cdot \frac{1}{1 + \frac{x - hi}{lo}} \]

5. Simplified 9.6%

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

   [Start] 9.6	\[ \left(1 - {\left(\frac{x - hi}{lo}\right)}^{2}\right) \cdot \frac{1}{1 + \frac{x - hi}{lo}} \]
   associate-*r/ [=>] 9.6	\[ \color{blue}{\frac{\left(1 - {\left(\frac{x - hi}{lo}\right)}^{2}\right) \cdot 1}{1 + \frac{x - hi}{lo}}} \]
   *-rgt-identity [=>] 9.6	\[ \frac{\color{blue}{1 - {\left(\frac{x - hi}{lo}\right)}^{2}}}{1 + \frac{x - hi}{lo}} \]

6. Taylor expanded in lo around inf 98.6%

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

7. Applied egg-rr 98.5%

   \[\leadsto \color{blue}{{\left(e^{3 \cdot \left(-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)\right)}\right)}^{0.3333333333333333}} \]
   Proof

   [Start] 98.6	\[ \frac{1}{1 + \frac{x - hi}{lo}} \]
   add-cbrt-cube [=>] 97.9	\[ \color{blue}{\sqrt[3]{\left(\frac{1}{1 + \frac{x - hi}{lo}} \cdot \frac{1}{1 + \frac{x - hi}{lo}}\right) \cdot \frac{1}{1 + \frac{x - hi}{lo}}}} \]
   pow1/3 [=>] 98.5	\[ \color{blue}{{\left(\left(\frac{1}{1 + \frac{x - hi}{lo}} \cdot \frac{1}{1 + \frac{x - hi}{lo}}\right) \cdot \frac{1}{1 + \frac{x - hi}{lo}}\right)}^{0.3333333333333333}} \]
   add-exp-log [=>] 98.4	\[ {\color{blue}{\left(e^{\log \left(\left(\frac{1}{1 + \frac{x - hi}{lo}} \cdot \frac{1}{1 + \frac{x - hi}{lo}}\right) \cdot \frac{1}{1 + \frac{x - hi}{lo}}\right)}\right)}}^{0.3333333333333333} \]
   pow3 [=>] 98.4	\[ {\left(e^{\log \color{blue}{\left({\left(\frac{1}{1 + \frac{x - hi}{lo}}\right)}^{3}\right)}}\right)}^{0.3333333333333333} \]
   log-pow [=>] 98.4	\[ {\left(e^{\color{blue}{3 \cdot \log \left(\frac{1}{1 + \frac{x - hi}{lo}}\right)}}\right)}^{0.3333333333333333} \]
   log-rec [=>] 98.4	\[ {\left(e^{3 \cdot \color{blue}{\left(-\log \left(1 + \frac{x - hi}{lo}\right)\right)}}\right)}^{0.3333333333333333} \]
   log1p-udef [<=] 98.5	\[ {\left(e^{3 \cdot \left(-\color{blue}{\mathsf{log1p}\left(\frac{x - hi}{lo}\right)}\right)}\right)}^{0.3333333333333333} \]

8. Simplified 98.7%

   \[\leadsto \color{blue}{e^{-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)}} \]
   Proof

   [Start] 98.5	\[ {\left(e^{3 \cdot \left(-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)\right)}\right)}^{0.3333333333333333} \]
   unpow1/3 [=>] 98.0	\[ \color{blue}{\sqrt[3]{e^{3 \cdot \left(-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)\right)}}} \]
   *-commutative [=>] 98.0	\[ \sqrt[3]{e^{\color{blue}{\left(-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)\right) \cdot 3}}} \]
   exp-prod [=>] 97.9	\[ \sqrt[3]{\color{blue}{{\left(e^{-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)}\right)}^{3}}} \]
   rem-cbrt-cube [=>] 98.7	\[ \color{blue}{e^{-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)}} \]

9. Final simplification 98.7%

   \[\leadsto e^{-\mathsf{log1p}\left(\frac{x - hi}{lo}\right)} \]

Alternatives

Alternative 1
Accuracy	98.4%
Cost	576

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

Alternative 2
Accuracy	98.4%
Cost	448

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

Alternative 3
Accuracy	18.8%
Cost	320

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

Alternative 4
Accuracy	18.8%
Cost	256

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

Alternative 5
Accuracy	18.7%
Cost	64

\[1 \]

Reproduce

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