Average Error: 37.3 → 23.7
Time: 13.3s
Precision: 64
\[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \cdot x + y \cdot y \le 1.234762663916167449450391070139532848652 \cdot 10^{-260}:\\ \;\;\;\;\left|\frac{1}{\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}} \cdot \frac{z}{\sqrt[3]{\sqrt{3}}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 3.457799854325248563136886079015659053076 \cdot 10^{297}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;\left|-\frac{x}{\sqrt{3}}\right|\\ \end{array}\]
\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}
↓
\begin{array}{l}
\mathbf{if}\;x \cdot x + y \cdot y \le 1.234762663916167449450391070139532848652 \cdot 10^{-260}:\\
\;\;\;\;\left|\frac{1}{\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}} \cdot \frac{z}{\sqrt[3]{\sqrt{3}}}\right|\\

\mathbf{elif}\;x \cdot x + y \cdot y \le 3.457799854325248563136886079015659053076 \cdot 10^{297}:\\
\;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\

\mathbf{else}:\\
\;\;\;\;\left|-\frac{x}{\sqrt{3}}\right|\\

\end{array}
double f(double x, double y, double z) {
        double r547178 = x;
        double r547179 = r547178 * r547178;
        double r547180 = y;
        double r547181 = r547180 * r547180;
        double r547182 = r547179 + r547181;
        double r547183 = z;
        double r547184 = r547183 * r547183;
        double r547185 = r547182 + r547184;
        double r547186 = 3.0;
        double r547187 = r547185 / r547186;
        double r547188 = sqrt(r547187);
        return r547188;
}
↓
double f(double x, double y, double z) {
        double r547189 = x;
        double r547190 = r547189 * r547189;
        double r547191 = y;
        double r547192 = r547191 * r547191;
        double r547193 = r547190 + r547192;
        double r547194 = 1.2347626639161674e-260;
        bool r547195 = r547193 <= r547194;
        double r547196 = 1.0;
        double r547197 = 3.0;
        double r547198 = sqrt(r547197);
        double r547199 = cbrt(r547198);
        double r547200 = r547199 * r547199;
        double r547201 = r547196 / r547200;
        double r547202 = z;
        double r547203 = r547202 / r547199;
        double r547204 = r547201 * r547203;
        double r547205 = fabs(r547204);
        double r547206 = 3.4577998543252486e+297;
        bool r547207 = r547193 <= r547206;
        double r547208 = r547202 * r547202;
        double r547209 = r547193 + r547208;
        double r547210 = sqrt(r547209);
        double r547211 = r547210 / r547198;
        double r547212 = fabs(r547211);
        double r547213 = r547189 / r547198;
        double r547214 = -r547213;
        double r547215 = fabs(r547214);
        double r547216 = r547207 ? r547212 : r547215;
        double r547217 = r547195 ? r547205 : r547216;
        return r547217;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original37.3
Target24.9
Herbie23.7
\[\begin{array}{l} \mathbf{if}\;z \lt -6.396479394109775845820908799933348003545 \cdot 10^{136}:\\ \;\;\;\;\frac{-z}{\sqrt{3}}\\ \mathbf{elif}\;z \lt 7.320293694404182125923160810847974073098 \cdot 10^{117}:\\ \;\;\;\;\frac{\sqrt{\left(z \cdot z + x \cdot x\right) + y \cdot y}}{\sqrt{3}}\\ \mathbf{else}:\\ \;\;\;\;\sqrt{0.3333333333333333148296162562473909929395} \cdot z\\ \end{array}\]

Derivation

  1. Split input into 3 regimes

  2. if (+ (* x x) (* y y)) < 1.2347626639161674e-260

    1. Initial program 25.5

      \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt25.7

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

    4. Applied add-sqr-sqrt25.7

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

    5. Applied times-frac25.6

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

    6. Applied rem-sqrt-square25.6

      \[\leadsto \color{blue}{\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|}\]

    7. Taylor expanded around 0 11.7

      \[\leadsto \left|\frac{\color{blue}{z}}{\sqrt{3}}\right|\]
    8. Using strategy rm

    9. Applied add-cube-cbrt11.7

      \[\leadsto \left|\frac{z}{\color{blue}{\left(\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}\right) \cdot \sqrt[3]{\sqrt{3}}}}\right|\]

    10. Applied *-un-lft-identity11.7

      \[\leadsto \left|\frac{\color{blue}{1 \cdot z}}{\left(\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}\right) \cdot \sqrt[3]{\sqrt{3}}}\right|\]

    11. Applied times-frac11.7

      \[\leadsto \left|\color{blue}{\frac{1}{\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}} \cdot \frac{z}{\sqrt[3]{\sqrt{3}}}}\right|\]

    if 1.2347626639161674e-260 < (+ (* x x) (* y y)) < 3.4577998543252486e+297

    1. Initial program 15.8

      \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt16.0

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

    4. Applied add-sqr-sqrt16.0

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

    5. Applied times-frac15.9

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

    6. Applied rem-sqrt-square15.9

      \[\leadsto \color{blue}{\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|}\]

    if 3.4577998543252486e+297 < (+ (* x x) (* y y))

    1. Initial program 62.8

      \[\sqrt{\frac{\left(x \cdot x + y \cdot y\right) + z \cdot z}{3}}\]
    2. Using strategy rm

    3. Applied add-sqr-sqrt62.8

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

    4. Applied add-sqr-sqrt62.8

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

    5. Applied times-frac62.8

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

    6. Applied rem-sqrt-square62.8

      \[\leadsto \color{blue}{\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|}\]

    7. Taylor expanded around -inf 34.3

      \[\leadsto \left|\color{blue}{-1 \cdot \frac{x}{\sqrt{3}}}\right|\]

    8. Simplified34.3

      \[\leadsto \left|\color{blue}{-\frac{x}{\sqrt{3}}}\right|\]
  3. Recombined 3 regimes into one program.

  4. Final simplification23.7

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot x + y \cdot y \le 1.234762663916167449450391070139532848652 \cdot 10^{-260}:\\ \;\;\;\;\left|\frac{1}{\sqrt[3]{\sqrt{3}} \cdot \sqrt[3]{\sqrt{3}}} \cdot \frac{z}{\sqrt[3]{\sqrt{3}}}\right|\\ \mathbf{elif}\;x \cdot x + y \cdot y \le 3.457799854325248563136886079015659053076 \cdot 10^{297}:\\ \;\;\;\;\left|\frac{\sqrt{\left(x \cdot x + y \cdot y\right) + z \cdot z}}{\sqrt{3}}\right|\\ \mathbf{else}:\\ \;\;\;\;\left|-\frac{x}{\sqrt{3}}\right|\\ \end{array}\]

Reproduce

herbie shell --seed 2019208 
(FPCore (x y z)
  :name "Data.Array.Repa.Algorithms.Pixel:doubleRmsOfRGB8 from repa-algorithms-3.4.0.1"
  :precision binary64

  :herbie-target
  (if (< z -6.3964793941097758e136) (/ (- z) (sqrt 3)) (if (< z 7.3202936944041821e117) (/ (sqrt (+ (+ (* z z) (* x x)) (* y y))) (sqrt 3)) (* (sqrt 0.333333333333333315) z)))

  (sqrt (/ (+ (+ (* x x) (* y y)) (* z z)) 3)))