Kahan p9 Example

Average Error: 19.7 → 5.0

Time: 14.8s

Precision: 64

\[0.0 \lt x \lt 1 \land y \lt 1\]

Math

\[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

↓

\[\begin{array}{l} \mathbf{if}\;y \le -1.576060656443760050067630439871422555514 \cdot 10^{153}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -7.512106064144896311879552836863591950545 \cdot 10^{-163}:\\ \;\;\;\;\frac{\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \left(\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}\right) - \left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}}{\left(\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y} + \sqrt[3]{\left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) + \frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}}\\ \mathbf{elif}\;y \le -9.739334495050348959786376614389218616652 \cdot 10^{-187}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le 6.255179780863846976704429693615073578173 \cdot 10^{-169}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \left(\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}\right) - \left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}}{\left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y} + \frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) + \frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}}\\ \end{array}\]

C

double f(double x, double y) {
        double r3653642 = x;
        double r3653643 = y;
        double r3653644 = r3653642 - r3653643;
        double r3653645 = r3653642 + r3653643;
        double r3653646 = r3653644 * r3653645;
        double r3653647 = r3653642 * r3653642;
        double r3653648 = r3653643 * r3653643;
        double r3653649 = r3653647 + r3653648;
        double r3653650 = r3653646 / r3653649;
        return r3653650;
}

↓

double f(double x, double y) {
        double r3653651 = y;
        double r3653652 = -1.57606065644376e+153;
        bool r3653653 = r3653651 <= r3653652;
        double r3653654 = -1.0;
        double r3653655 = -7.512106064144896e-163;
        bool r3653656 = r3653651 <= r3653655;
        double r3653657 = x;
        double r3653658 = r3653657 * r3653657;
        double r3653659 = r3653651 * r3653651;
        double r3653660 = r3653658 + r3653659;
        double r3653661 = r3653658 / r3653660;
        double r3653662 = r3653661 * r3653661;
        double r3653663 = r3653661 * r3653662;
        double r3653664 = r3653659 / r3653660;
        double r3653665 = r3653664 * r3653664;
        double r3653666 = r3653665 * r3653664;
        double r3653667 = r3653663 - r3653666;
        double r3653668 = r3653661 * r3653664;
        double r3653669 = cbrt(r3653666);
        double r3653670 = r3653669 * r3653664;
        double r3653671 = r3653668 + r3653670;
        double r3653672 = r3653671 + r3653662;
        double r3653673 = r3653667 / r3653672;
        double r3653674 = -9.739334495050349e-187;
        bool r3653675 = r3653651 <= r3653674;
        double r3653676 = 6.255179780863847e-169;
        bool r3653677 = r3653651 <= r3653676;
        double r3653678 = 1.0;
        double r3653679 = r3653665 + r3653668;
        double r3653680 = r3653679 + r3653662;
        double r3653681 = r3653667 / r3653680;
        double r3653682 = r3653677 ? r3653678 : r3653681;
        double r3653683 = r3653675 ? r3653654 : r3653682;
        double r3653684 = r3653656 ? r3653673 : r3653683;
        double r3653685 = r3653653 ? r3653654 : r3653684;
        return r3653685;
}

Error

Bits error versus x

Bits error versus y

Target

Original	19.7
Target	0.1
Herbie	5.0

\[\begin{array}{l} \mathbf{if}\;0.5 \lt \left|\frac{x}{y}\right| \lt 2:\\ \;\;\;\;\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{2}{1 + \frac{x}{y} \cdot \frac{x}{y}}\\ \end{array}\]

Derivation

1. Split input into 4 regimes

2. if y < -1.57606065644376e+153 or -7.512106064144896e-163 < y < -9.739334495050349e-187

   1. Initial program 59.2

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

   2. Simplified 59.2

      \[\leadsto \color{blue}{\frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y \cdot y}{x \cdot x + y \cdot y}}\]

   3. Taylor expanded around 0 4.6

      \[\leadsto \color{blue}{-1}\]

   if -1.57606065644376e+153 < y < -7.512106064144896e-163

   1. Initial program 0.1

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

   2. Simplified 0.1

      \[\leadsto \color{blue}{\frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y \cdot y}{x \cdot x + y \cdot y}}\]
   3. Using strategy rm

   4. Applied flip3-- 0.1

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

   5. Simplified 0.1

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

   7. Applied add-cbrt-cube 0.1

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

   if -9.739334495050349e-187 < y < 6.255179780863847e-169

   1. Initial program 28.6

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

   2. Simplified 28.6

      \[\leadsto \color{blue}{\frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y \cdot y}{x \cdot x + y \cdot y}}\]

   3. Taylor expanded around inf 13.6

      \[\leadsto \color{blue}{1}\]

   if 6.255179780863847e-169 < y

   1. Initial program 1.5

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]

   2. Simplified 1.5

      \[\leadsto \color{blue}{\frac{x \cdot x}{x \cdot x + y \cdot y} - \frac{y \cdot y}{x \cdot x + y \cdot y}}\]
   3. Using strategy rm

   4. Applied flip3-- 1.5

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

   5. Simplified 1.5

      \[\leadsto \frac{\color{blue}{\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \left(\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}\right) - \frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right)}}{\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y} + \left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y} + \frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right)}\]
3. Recombined 4 regimes into one program.

4. Final simplification 5.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.576060656443760050067630439871422555514 \cdot 10^{153}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -7.512106064144896311879552836863591950545 \cdot 10^{-163}:\\ \;\;\;\;\frac{\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \left(\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}\right) - \left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}}{\left(\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y} + \sqrt[3]{\left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) + \frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}}\\ \mathbf{elif}\;y \le -9.739334495050348959786376614389218616652 \cdot 10^{-187}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le 6.255179780863846976704429693615073578173 \cdot 10^{-169}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \left(\frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}\right) - \left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}}{\left(\frac{y \cdot y}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y} + \frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{y \cdot y}{x \cdot x + y \cdot y}\right) + \frac{x \cdot x}{x \cdot x + y \cdot y} \cdot \frac{x \cdot x}{x \cdot x + y \cdot y}}\\ \end{array}\]

Reproduce

herbie shell --seed 2019179 
(FPCore (x y)
  :name "Kahan p9 Example"
  :pre (and (< 0.0 x 1.0) (< y 1.0))

  :herbie-target
  (if (< 0.5 (fabs (/ x y)) 2.0) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- 1.0 (/ 2.0 (+ 1.0 (* (/ x y) (/ x y))))))

  (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))))