Main:z from

Average Error: 5.5 → 4.2

Time: 11.3s

Precision: binary64

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)\]

↓

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

C

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

↓

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

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	5.5
Target	1.6
Herbie	4.2

\[\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. Initial program 5.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. Using strategy rm

3. Applied flip-- 5.4

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

4. Simplified 5.2

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

5. Taylor expanded around 0 4.2

   \[\leadsto \left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \frac{\color{blue}{1}}{\sqrt{y + 1} + \sqrt{y}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\]
6. Using strategy rm

7. Applied add-sqr-sqrt 4.2

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

8. Applied associate-/r* 4.2

   \[\leadsto \left(\left(\left(\sqrt{x + 1} - \sqrt{x}\right) + \color{blue}{\frac{\frac{1}{\sqrt{\sqrt{y + 1} + \sqrt{y}}}}{\sqrt{\sqrt{y + 1} + \sqrt{y}}}}\right) + \left(\sqrt{z + 1} - \sqrt{z}\right)\right) + \left(\sqrt{t + 1} - \sqrt{t}\right)\]
9. Using strategy rm

10. Applied add-sqr-sqrt 4.2

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

11. Applied sqrt-prod 4.2

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

12. Applied *-un-lft-identity 4.2

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

13. Applied times-frac 4.2

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

14. Applied associate-/l* 4.2

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

15. Final simplification 4.2

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

Reproduce

herbie shell --seed 2020171 
(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))))