Kahan p9 Example

1. Initial program 77.0%

   \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
2. Step-by-step derivation

   1. add-sqr-sqrt76.9%

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

   2. times-frac76.6%

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

   3. hypot-def76.6%

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

   4. hypot-def100.0%

      \[\leadsto \frac{x - y}{\mathsf{hypot}\left(x, y\right)} \cdot \frac{x + y}{\color{blue}{\mathsf{hypot}\left(x, y\right)}} \]

3. Applied egg-rr100.0%

   \[\leadsto \color{blue}{\frac{x - y}{\mathsf{hypot}\left(x, y\right)} \cdot \frac{x + y}{\mathsf{hypot}\left(x, y\right)}} \]

4. Final simplification100.0%

   \[\leadsto \frac{x - y}{\mathsf{hypot}\left(x, y\right)} \cdot \frac{x + y}{\mathsf{hypot}\left(x, y\right)} \]

1. Split input into 2 regimes

2. if (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) < 2

   1. Initial program 100.0%

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

   if 2 < (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))

   1. Initial program 0.0%

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

   2. Taylor expanded in y around inf 55.9%

      \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} + \left(\frac{x}{y} + -1 \cdot \frac{x}{y}\right)\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
   3. Step-by-step derivation

      1. distribute-rgt1-in55.9%

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

      2. metadata-eval55.9%

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

      3. associate-*r/55.9%

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

      4. mul0-lft55.9%

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

      5. metadata-eval55.9%

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

      6. mul0-lft55.9%

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

      7. metadata-eval55.9%

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

      8. distribute-lft1-in55.9%

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

      9. associate-*r/55.9%

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

      10. associate--r+55.9%

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

      11. sub-neg55.9%

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

   4. Simplified74.5%

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

4. Final simplification94.1%

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

1. Split input into 3 regimes

2. if y < -4.19999999999999996e-163

   1. Initial program 76.9%

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

   2. Taylor expanded in x around 0 91.6%

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

   if -4.19999999999999996e-163 < y < 2.74999999999999993e-126

   1. Initial program 65.8%

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

   2. Taylor expanded in x around inf 84.0%

      \[\leadsto \color{blue}{\frac{y}{x} + \left(1 + -1 \cdot \frac{y}{x}\right)} \]
   3. Step-by-step derivation

      1. mul-1-neg84.0%

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

      2. unsub-neg84.0%

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

   4. Simplified84.0%

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

   if 2.74999999999999993e-126 < y

   1. Initial program 100.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
   2. Step-by-step derivation

      1. associate-/l*99.8%

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

      2. fma-def99.8%

         \[\leadsto \frac{x - y}{\frac{\color{blue}{\mathsf{fma}\left(x, x, y \cdot y\right)}}{x + y}} \]

   3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{x - y}{\frac{\mathsf{fma}\left(x, x, y \cdot y\right)}{x + y}}} \]

   4. Taylor expanded in x around 0 72.6%

      \[\leadsto \frac{x - y}{\color{blue}{y}} \]
3. Recombined 3 regimes into one program.

4. Final simplification86.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -4.2 \cdot 10^{-163}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \leq 2.75 \cdot 10^{-126}:\\ \;\;\;\;\frac{y}{x} + \left(1 - \frac{y}{x}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{x - y}{y}\\ \end{array} \]

1. Split input into 3 regimes

2. if y < -1.52000000000000002e-161

   1. Initial program 76.9%

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

   2. Taylor expanded in x around 0 91.6%

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

   if -1.52000000000000002e-161 < y < 2.8e-125

   1. Initial program 65.8%

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

   2. Taylor expanded in x around inf 84.0%

      \[\leadsto \color{blue}{\frac{y}{x} + \left(1 + -1 \cdot \frac{y}{x}\right)} \]
   3. Step-by-step derivation

      1. mul-1-neg84.0%

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

      2. unsub-neg84.0%

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

   4. Simplified84.0%

      \[\leadsto \color{blue}{\frac{y}{x} + \left(1 - \frac{y}{x}\right)} \]
   5. Step-by-step derivation

      1. associate-+r-84.0%

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

   6. Applied egg-rr84.0%

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

   if 2.8e-125 < y

   1. Initial program 100.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
   2. Step-by-step derivation

      1. associate-/l*99.8%

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

      2. fma-def99.8%

         \[\leadsto \frac{x - y}{\frac{\color{blue}{\mathsf{fma}\left(x, x, y \cdot y\right)}}{x + y}} \]

   3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{x - y}{\frac{\mathsf{fma}\left(x, x, y \cdot y\right)}{x + y}}} \]

   4. Taylor expanded in x around 0 72.6%

      \[\leadsto \frac{x - y}{\color{blue}{y}} \]
3. Recombined 3 regimes into one program.

4. Final simplification86.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -1.52 \cdot 10^{-161}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \leq 2.8 \cdot 10^{-125}:\\ \;\;\;\;\left(\frac{y}{x} + 1\right) - \frac{y}{x}\\ \mathbf{else}:\\ \;\;\;\;\frac{x - y}{y}\\ \end{array} \]

1. Split input into 3 regimes

2. if y < -1.80000000000000004e-179

   1. Initial program 76.2%

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

   2. Taylor expanded in y around inf 89.7%

      \[\leadsto \color{blue}{\left(\frac{{x}^{2}}{{y}^{2}} + \left(\frac{x}{y} + -1 \cdot \frac{x}{y}\right)\right) - \left(-1 \cdot \frac{{x}^{2}}{{y}^{2}} + 1\right)} \]
   3. Step-by-step derivation

      1. distribute-rgt1-in89.7%

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

      2. metadata-eval89.7%

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

      3. associate-*r/89.7%

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

      4. mul0-lft89.7%

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

      5. metadata-eval89.7%

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

      6. mul0-lft89.7%

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

      7. metadata-eval89.7%

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

      8. distribute-lft1-in89.7%

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

      9. associate-*r/89.7%

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

      10. associate--r+89.7%

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

      11. sub-neg89.7%

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

   4. Simplified91.1%

      \[\leadsto \color{blue}{\left(0 + 2 \cdot \left(\frac{x}{y} \cdot \frac{x}{y}\right)\right) + -1} \]

   if -1.80000000000000004e-179 < y < 6.2e-127

   1. Initial program 66.7%

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

   2. Taylor expanded in x around inf 85.8%

      \[\leadsto \color{blue}{\frac{y}{x} + \left(1 + -1 \cdot \frac{y}{x}\right)} \]
   3. Step-by-step derivation

      1. mul-1-neg85.8%

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

      2. unsub-neg85.8%

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

   4. Simplified85.8%

      \[\leadsto \color{blue}{\frac{y}{x} + \left(1 - \frac{y}{x}\right)} \]
   5. Step-by-step derivation

      1. associate-+r-85.9%

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

   6. Applied egg-rr85.9%

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

   if 6.2e-127 < y

   1. Initial program 100.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
   2. Step-by-step derivation

      1. associate-/l*99.8%

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

      2. fma-def99.8%

         \[\leadsto \frac{x - y}{\frac{\color{blue}{\mathsf{fma}\left(x, x, y \cdot y\right)}}{x + y}} \]

   3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{x - y}{\frac{\mathsf{fma}\left(x, x, y \cdot y\right)}{x + y}}} \]

   4. Taylor expanded in x around 0 72.6%

      \[\leadsto \frac{x - y}{\color{blue}{y}} \]
3. Recombined 3 regimes into one program.

4. Final simplification87.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -1.8 \cdot 10^{-179}:\\ \;\;\;\;2 \cdot \left(\frac{x}{y} \cdot \frac{x}{y}\right) + -1\\ \mathbf{elif}\;y \leq 6.2 \cdot 10^{-127}:\\ \;\;\;\;\left(\frac{y}{x} + 1\right) - \frac{y}{x}\\ \mathbf{else}:\\ \;\;\;\;\frac{x - y}{y}\\ \end{array} \]

1. Split input into 3 regimes

2. if y < -1.1e-160

   1. Initial program 76.9%

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

   2. Taylor expanded in x around 0 91.6%

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

   if -1.1e-160 < y < 2.4999999999999999e-127

   1. Initial program 65.8%

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

   2. Taylor expanded in x around inf 83.8%

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

   if 2.4999999999999999e-127 < y

   1. Initial program 100.0%

      \[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y} \]
   2. Step-by-step derivation

      1. associate-/l*99.8%

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

      2. fma-def99.8%

         \[\leadsto \frac{x - y}{\frac{\color{blue}{\mathsf{fma}\left(x, x, y \cdot y\right)}}{x + y}} \]

   3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{x - y}{\frac{\mathsf{fma}\left(x, x, y \cdot y\right)}{x + y}}} \]

   4. Taylor expanded in x around 0 72.6%

      \[\leadsto \frac{x - y}{\color{blue}{y}} \]
3. Recombined 3 regimes into one program.

4. Final simplification86.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -1.1 \cdot 10^{-160}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \leq 2.5 \cdot 10^{-127}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;\frac{x - y}{y}\\ \end{array} \]

1. Split input into 2 regimes

2. if y < -7.9999999999999999e-160 or 2.0000000000000001e-114 < y

   1. Initial program 81.3%

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

   2. Taylor expanded in x around 0 88.2%

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

   if -7.9999999999999999e-160 < y < 2.0000000000000001e-114

   1. Initial program 67.5%

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

   2. Taylor expanded in x around inf 82.2%

      \[\leadsto \color{blue}{1} \]
3. Recombined 2 regimes into one program.

4. Final simplification86.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -8 \cdot 10^{-160}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \leq 2 \cdot 10^{-114}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;-1\\ \end{array} \]

1. Initial program 77.0%

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

2. Taylor expanded in x around 0 66.4%

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

3. Final simplification66.4%

   \[\leadsto -1 \]

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

  :herbie-target
  (if (and (< 0.5 (fabs (/ x y))) (< (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))))