Error

Derivation

1. Split input into 2 regimes

2. if re < 0.063018798828125

   1. Initial program 0.7

      \[\left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \left(\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right) - re\right)\right)}\right)\]

   if 0.063018798828125 < re

   1. Initial program 3.9

      \[\left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \left(\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right) - re\right)\right)}\right)\]
   2. Using strategy rm

   3. Applied p16-flip--3.5

      \[\leadsto \left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \color{blue}{\left(\frac{\left(\left(\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right) \cdot \left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)\right) - \left(re \cdot re\right)\right)}{\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)}\right)}\right)}\right)\]
   4. Using strategy rm

   5. Applied difference-of-squares3.9

      \[\leadsto \left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \left(\frac{\color{blue}{\left(\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right) \cdot \left(\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right) - re\right)\right)}}{\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)}\right)\right)}\right)\]
   6. Using strategy rm

   7. Applied p16-flip--3.5

      \[\leadsto \left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \left(\frac{\left(\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right) \cdot \color{blue}{\left(\frac{\left(\left(\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right) \cdot \left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)\right) - \left(re \cdot re\right)\right)}{\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)}\right)}\right)}{\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)}\right)\right)}\right)\]

   8. Applied associate-*r/4.0

      \[\leadsto \left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \left(\frac{\color{blue}{\left(\frac{\left(\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right) \cdot \left(\left(\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right) \cdot \left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)\right) - \left(re \cdot re\right)\right)\right)}{\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)}\right)}}{\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)}\right)\right)}\right)\]

   9. Applied associate-/l/4.0

      \[\leadsto \left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \color{blue}{\left(\frac{\left(\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right) \cdot \left(\left(\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right) \cdot \left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)\right) - \left(re \cdot re\right)\right)\right)}{\left(\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right) \cdot \left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)\right)}\right)}\right)}\right)\]

   10. Simplified1.8

       \[\leadsto \left(real->posit(0.5)\right) \cdot \left(\sqrt{\left(\left(real->posit(2.0)\right) \cdot \left(\frac{\color{blue}{\left(\left(\frac{re}{\left(\sqrt{\left(\frac{\left(im \cdot im\right)}{\left(re \cdot re\right)}\right)}\right)}\right) \cdot \left(im \cdot im\right)\right)}}{\left(\left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right) \cdot \left(\frac{\left(\sqrt{\left(\frac{\left(re \cdot re\right)}{\left(im \cdot im\right)}\right)}\right)}{re}\right)\right)}\right)\right)}\right)\]

   11. Simplified0.9

       \[\leadsto \color{blue}{\left(\sqrt{\left(\left(\frac{\left(real->posit(2.0)\right)}{\left(\frac{\left(\sqrt{\left(\frac{\left(im \cdot im\right)}{\left(re \cdot re\right)}\right)}\right)}{re}\right)}\right) \cdot \left(\left(real->posit(1.0)\right) \cdot \left(im \cdot im\right)\right)\right)}\right) \cdot \left(real->posit(0.5)\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification0.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;re \le 0.063018798828125:\\ \;\;\;\;0.5 \cdot \sqrt{2.0 \cdot \left(\sqrt{re \cdot re + im \cdot im} - re\right)}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{2.0}{\sqrt{im \cdot im + re \cdot re} + re} \cdot \left(1.0 \cdot \left(im \cdot im\right)\right)} \cdot 0.5\\ \end{array}\]

Reproduce

herbie shell --seed 2019091 +o rules:numerics
(FPCore (re im)
  :name "math.sqrt on complex, imaginary part, im greater than 0 branch"
  (*.p16 (real->posit16 0.5) (sqrt.p16 (*.p16 (real->posit16 2.0) (-.p16 (sqrt.p16 (+.p16 (*.p16 re re) (*.p16 im im))) re)))))