(- x (* (/ (/ (sqrt x) 1) 2) (sqrt x)))

Average Error: 0.5 → 0

Time: 896.0ms

Precision: binary64

• could not determine a ground truth for program body

  1. x = 1.847630465521513e-308

Math

\[x - \frac{\frac{\sqrt{x}}{1}}{2} \cdot \sqrt{x}\]

↓

\[x - \frac{\frac{x}{2}}{1}\]

C

double code(double x) {
	return ((double) (x - ((double) (((double) (((double) (((double) sqrt(x)) / 1.0)) / 2.0)) * ((double) sqrt(x))))));
}

↓

double code(double x) {
	return ((double) (x - ((double) (((double) (x / 2.0)) / 1.0))));
}

Error

Bits error versus x

Derivation

1. Initial program 0.5

   \[x - \frac{\frac{\sqrt{x}}{1}}{2} \cdot \sqrt{x}\]

2. Simplified 0

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

3. Final simplification 0

   \[\leadsto x - \frac{\frac{x}{2}}{1}\]

Reproduce

herbie shell --seed 2020152 
(FPCore (x)
  :name "(- x (* (/ (/ (sqrt x) 1) 2) (sqrt x)))"
  :precision binary64
  (- x (* (/ (/ (sqrt x) 1.0) 2.0) (sqrt x))))