Main:z from

Average Error: 5.4 → 2.8

Time: 15.1s

Precision: binary64

\[[x, y, z, t] = \mathsf{sort}([x, y, z, t]) \\]

Math

\[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

↓

\[\begin{array}{l} t_1 := \sqrt{z + 1} - \sqrt{z}\\ t_2 := \sqrt{x + 1} - \sqrt{x}\\ t_3 := \sqrt{t + 1} - \sqrt{t}\\ t_4 := \sqrt{y + 1} - \sqrt{y}\\ \mathbf{if}\;t_2 + t_4 \leq 8.897623047232628 \cdot 10^{-7}:\\ \;\;\;\;\left(\left(\frac{0.375 \cdot \sqrt{\frac{1}{x}} + 1.5 \cdot \sqrt{x}}{\left(1 + x\right) + \left(x + \sqrt{\left(1 + x\right) \cdot x}\right)} + t_4\right) + t_1\right) + t_3\\ \mathbf{else}:\\ \;\;\;\;\left(\left(t_2 + \log \left(1 + \mathsf{expm1}\left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + t_1\right) + t_3\\ \end{array} \]

FPCore

(FPCore (x y z t)
 :precision binary64
 (+
  (+
   (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y)))
   (- (sqrt (+ z 1.0)) (sqrt z)))
  (- (sqrt (+ t 1.0)) (sqrt t))))

↓

(FPCore (x y z t)
 :precision binary64
 (let* ((t_1 (- (sqrt (+ z 1.0)) (sqrt z)))
        (t_2 (- (sqrt (+ x 1.0)) (sqrt x)))
        (t_3 (- (sqrt (+ t 1.0)) (sqrt t)))
        (t_4 (- (sqrt (+ y 1.0)) (sqrt y))))
   (if (<= (+ t_2 t_4) 8.897623047232628e-7)
     (+
      (+
       (+
        (/
         (+ (* 0.375 (sqrt (/ 1.0 x))) (* 1.5 (sqrt x)))
         (+ (+ 1.0 x) (+ x (sqrt (* (+ 1.0 x) x)))))
        t_4)
       t_1)
      t_3)
     (+
      (+ (+ t_2 (log (+ 1.0 (expm1 (- (sqrt (+ 1.0 y)) (sqrt y)))))) t_1)
      t_3))))

C

double code(double x, double y, double z, double t) {
	return (((sqrt((x + 1.0)) - sqrt(x)) + (sqrt((y + 1.0)) - sqrt(y))) + (sqrt((z + 1.0)) - sqrt(z))) + (sqrt((t + 1.0)) - sqrt(t));
}

↓

double code(double x, double y, double z, double t) {
	double t_1 = sqrt((z + 1.0)) - sqrt(z);
	double t_2 = sqrt((x + 1.0)) - sqrt(x);
	double t_3 = sqrt((t + 1.0)) - sqrt(t);
	double t_4 = sqrt((y + 1.0)) - sqrt(y);
	double tmp;
	if ((t_2 + t_4) <= 8.897623047232628e-7) {
		tmp = (((((0.375 * sqrt((1.0 / x))) + (1.5 * sqrt(x))) / ((1.0 + x) + (x + sqrt(((1.0 + x) * x))))) + t_4) + t_1) + t_3;
	} else {
		tmp = ((t_2 + log((1.0 + expm1((sqrt((1.0 + y)) - sqrt(y)))))) + t_1) + t_3;
	}
	return tmp;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	5.4
Target	0.4
Herbie	2.8

\[\left(\left(\frac{1}{\sqrt{x + 1} + \sqrt{x}} + \frac{1}{\sqrt{y + 1} + \sqrt{y}}\right) + \frac{1}{\sqrt{z + 1} + \sqrt{z}}\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

Derivation

1. Split input into 2 regimes

2. if (+.f64 (-.f64 (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y 1)) (sqrt.f64 y))) < 8.89762e-7

   1. Initial program 60.5

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   2. Applied egg-rr 60.4

      \[\leadsto \left(\left(\color{blue}{\frac{{\left(1 + x\right)}^{1.5} - {x}^{1.5}}{\left(1 + x\right) + \left(x + \sqrt{\left(1 + x\right) \cdot x}\right)}} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   3. Taylor expanded in x around inf 12.7

      \[\leadsto \left(\left(\frac{\color{blue}{0.375 \cdot \sqrt{\frac{1}{x}} + 1.5 \cdot \sqrt{x}}}{\left(1 + x\right) + \left(x + \sqrt{\left(1 + x\right) \cdot x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   if 8.89762e-7 < (+.f64 (-.f64 (sqrt.f64 (+.f64 x 1)) (sqrt.f64 x)) (-.f64 (sqrt.f64 (+.f64 y 1)) (sqrt.f64 y)))

   1. Initial program 2.2

      \[\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]

   2. Applied egg-rr 2.2

      \[\leadsto \left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \color{blue}{\log \left(1 + \mathsf{expm1}\left(\sqrt{1 + y} - \sqrt{y}\right)\right)}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right) \]
3. Recombined 2 regimes into one program.

4. Final simplification 2.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(\sqrt{x + 1} - \sqrt{x}\right) + \left(\sqrt{y + 1} - \sqrt{y}\right) \leq 8.897623047232628 \cdot 10^{-7}:\\ \;\;\;\;\left(\left(\frac{0.375 \cdot \sqrt{\frac{1}{x}} + 1.5 \cdot \sqrt{x}}{\left(1 + x\right) + \left(x + \sqrt{\left(1 + x\right) \cdot x}\right)} + \left(\sqrt{y + 1} - \sqrt{y}\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \log \left(1 + \mathsf{expm1}\left(\sqrt{1 + y} - \sqrt{y}\right)\right)\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\\ \end{array} \]

Reproduce

herbie shell --seed 2022127 
(FPCore (x y z t)
  :name "Main:z from "
  :precision binary64

  :herbie-target
  (+ (+ (+ (/ 1.0 (+ (sqrt (+ x 1.0)) (sqrt x))) (/ 1.0 (+ (sqrt (+ y 1.0)) (sqrt y)))) (/ 1.0 (+ (sqrt (+ z 1.0)) (sqrt z)))) (- (sqrt (+ t 1.0)) (sqrt t)))

  (+ (+ (+ (- (sqrt (+ x 1.0)) (sqrt x)) (- (sqrt (+ y 1.0)) (sqrt y))) (- (sqrt (+ z 1.0)) (sqrt z))) (- (sqrt (+ t 1.0)) (sqrt t))))