Migdal et al, Equation (51)

Percentage Accurate: 99.5% → 99.5%

Time: 10.0s

Alternatives: 9

Speedup: 1.1×

• Could not converge on a ground truth

  1. k = 2.294175699573734e+28
  2. n = -25916395739.522163

Specification

Math

\[\begin{array}{l} \\ \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (* (/ 1.0 (sqrt k)) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0))))

Initial Program: 99.5% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (* (/ 1.0 (sqrt k)) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0))))

Alternative 1: 99.5% accurate, 0.7× speedup

Math

\[\begin{array}{l} \\ {k}^{-0.5} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (* (pow k -0.5) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0))))

Derivation

1. Initial program 99.6%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Add Preprocessing
3. Step-by-step derivation

   1. lift-/.f64 N/A

      \[\leadsto \color{blue}{\frac{1}{\sqrt{k}}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   2. inv-pow N/A

      \[\leadsto \color{blue}{{\left(\sqrt{k}\right)}^{-1}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   3. lift-sqrt.f64 N/A

      \[\leadsto {\color{blue}{\left(\sqrt{k}\right)}}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   4. pow1/2 N/A

      \[\leadsto {\color{blue}{\left({k}^{\frac{1}{2}}\right)}}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   5. pow-pow N/A

      \[\leadsto \color{blue}{{k}^{\left(\frac{1}{2} \cdot -1\right)}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   6. lower-pow.f64 N/A

      \[\leadsto \color{blue}{{k}^{\left(\frac{1}{2} \cdot -1\right)}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

   7. metadata-eval 99.6

      \[\leadsto {k}^{\color{blue}{-0.5}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]

4. Applied rewrites 99.6%

   \[\leadsto \color{blue}{{k}^{-0.5}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
5. Add Preprocessing

Alternative 2: 97.9% accurate, 0.2× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := {\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)}\\ \mathbf{if}\;t\_0 \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{elif}\;t\_0 \leq 5 \cdot 10^{+284}:\\ \;\;\;\;\frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\sqrt{k}}\\ \mathbf{else}:\\ \;\;\;\;\frac{{0}^{\left(-k\right)}}{\sqrt{k}}\\ \end{array} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (let* ((t_0
         (* (pow (sqrt k) -1.0) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0)))))
   (if (<= t_0 5e-227)
     0.0
     (if (<= t_0 5e+284)
       (/ (sqrt (* (* n 2.0) (PI))) (sqrt k))
       (/ (pow 0.0 (- k)) (sqrt k))))))

Derivation

1. Split input into 3 regimes

2. if (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64)))) < 4.99999999999999961e-227

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   4. Applied rewrites 1.6%

      \[\leadsto \color{blue}{\frac{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}}} \]
   5. Step-by-step derivation

      1. lift-pow.f64 N/A

         \[\leadsto \frac{\color{blue}{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}}{\sqrt{k}} \]

      2. lift-*.f64 N/A

         \[\leadsto \frac{{\color{blue}{\left(0 \cdot n\right)}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      3. mul0-lft N/A

         \[\leadsto \frac{{\color{blue}{0}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      4. pow-base-0 98.0

         \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   6. Applied rewrites 98.0%

      \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   7. Taylor expanded in k around 0

      \[\leadsto \color{blue}{0} \]
   8. Step-by-step derivation

   9. Applied rewrites 98.0%

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

   if 4.99999999999999961e-227 < (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64)))) < 4.9999999999999999e284

   1. Initial program 99.3%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around 0

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \cdot \sqrt{2}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      3. lower-sqrt.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      6. *-commutative N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      7. lower-*.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      8. lower-PI.f64 71.1

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot n}{k}} \]

   5. Applied rewrites 71.1%

      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{\mathsf{PI}\left(\right) \cdot n}{k}}} \]
   6. Step-by-step derivation

   7. Applied rewrites 98.6%

      \[\leadsto \frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\color{blue}{\sqrt{k}}} \]

   if 4.9999999999999999e284 < (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64))))

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   4. Applied rewrites 100.0%

      \[\leadsto \color{blue}{\frac{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}}} \]

   5. Taylor expanded in k around inf

      \[\leadsto \frac{\color{blue}{e^{\frac{1}{8} \cdot \left(\log 0 \cdot \left(1 - k\right)\right)}}}{\sqrt{k}} \]
   6. Step-by-step derivation

      1. associate-*r* N/A

         \[\leadsto \frac{e^{\color{blue}{\left(\frac{1}{8} \cdot \log 0\right) \cdot \left(1 - k\right)}}}{\sqrt{k}} \]

      2. exp-prod N/A

         \[\leadsto \frac{\color{blue}{{\left(e^{\frac{1}{8} \cdot \log 0}\right)}^{\left(1 - k\right)}}}{\sqrt{k}} \]

      3. *-commutative N/A

         \[\leadsto \frac{{\left(e^{\color{blue}{\log 0 \cdot \frac{1}{8}}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      4. metadata-eval N/A

         \[\leadsto \frac{{\left(e^{\log \color{blue}{\left(\frac{1}{16} \cdot 0\right)} \cdot \frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      5. mul0-lft N/A

         \[\leadsto \frac{{\left(e^{\log \left(\frac{1}{16} \cdot \color{blue}{\left(0 \cdot \mathsf{NAN}\left(\right)\right)}\right) \cdot \frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      6. metadata-eval N/A

         \[\leadsto \frac{{\left(e^{\log \left(\frac{1}{16} \cdot \left(\color{blue}{\left(-1 + 1\right)} \cdot \mathsf{NAN}\left(\right)\right)\right) \cdot \frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      7. distribute-rgt1-in N/A

         \[\leadsto \frac{{\left(e^{\log \left(\frac{1}{16} \cdot \color{blue}{\left(\mathsf{NAN}\left(\right) + -1 \cdot \mathsf{NAN}\left(\right)\right)}\right) \cdot \frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      8. exp-to-pow N/A

         \[\leadsto \frac{{\color{blue}{\left({\left(\frac{1}{16} \cdot \left(\mathsf{NAN}\left(\right) + -1 \cdot \mathsf{NAN}\left(\right)\right)\right)}^{\frac{1}{8}}\right)}}^{\left(1 - k\right)}}{\sqrt{k}} \]

      9. distribute-rgt1-in N/A

         \[\leadsto \frac{{\left({\left(\frac{1}{16} \cdot \color{blue}{\left(\left(-1 + 1\right) \cdot \mathsf{NAN}\left(\right)\right)}\right)}^{\frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      10. metadata-eval N/A

          \[\leadsto \frac{{\left({\left(\frac{1}{16} \cdot \left(\color{blue}{0} \cdot \mathsf{NAN}\left(\right)\right)\right)}^{\frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      11. mul0-lft N/A

          \[\leadsto \frac{{\left({\left(\frac{1}{16} \cdot \color{blue}{0}\right)}^{\frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      12. metadata-eval N/A

          \[\leadsto \frac{{\left({\color{blue}{0}}^{\frac{1}{8}}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      13. metadata-eval N/A

          \[\leadsto \frac{{\color{blue}{0}}^{\left(1 - k\right)}}{\sqrt{k}} \]

      14. metadata-eval N/A

          \[\leadsto \frac{{\color{blue}{\left(\frac{1}{16} \cdot 0\right)}}^{\left(1 - k\right)}}{\sqrt{k}} \]

      15. mul0-lft N/A

          \[\leadsto \frac{{\left(\frac{1}{16} \cdot \color{blue}{\left(0 \cdot \mathsf{NAN}\left(\right)\right)}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      16. metadata-eval N/A

          \[\leadsto \frac{{\left(\frac{1}{16} \cdot \left(\color{blue}{\left(-1 + 1\right)} \cdot \mathsf{NAN}\left(\right)\right)\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      17. distribute-rgt1-in N/A

          \[\leadsto \frac{{\left(\frac{1}{16} \cdot \color{blue}{\left(\mathsf{NAN}\left(\right) + -1 \cdot \mathsf{NAN}\left(\right)\right)}\right)}^{\left(1 - k\right)}}{\sqrt{k}} \]

      18. lower-pow.f64 N/A

          \[\leadsto \frac{\color{blue}{{\left(\frac{1}{16} \cdot \left(\mathsf{NAN}\left(\right) + -1 \cdot \mathsf{NAN}\left(\right)\right)\right)}^{\left(1 - k\right)}}}{\sqrt{k}} \]

   7. Applied rewrites 100.0%

      \[\leadsto \frac{\color{blue}{{0}^{\left(1 - k\right)}}}{\sqrt{k}} \]

   8. Taylor expanded in k around inf

      \[\leadsto \frac{{0}^{\left(-1 \cdot \color{blue}{k}\right)}}{\sqrt{k}} \]
   9. Step-by-step derivation

   10. Applied rewrites 100.0%

       \[\leadsto \frac{{0}^{\left(-k\right)}}{\sqrt{k}} \]
3. Recombined 3 regimes into one program.

4. Final simplification 98.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{elif}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{+284}:\\ \;\;\;\;\frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\sqrt{k}}\\ \mathbf{else}:\\ \;\;\;\;\frac{{0}^{\left(-k\right)}}{\sqrt{k}}\\ \end{array} \]
5. Add Preprocessing

Alternative 3: 63.9% accurate, 0.3× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} t_0 := {\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)}\\ \mathbf{if}\;t\_0 \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{elif}\;t\_0 \leq 2 \cdot 10^{+153}:\\ \;\;\;\;\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k} \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{n + n}}{\sqrt{k}}\\ \end{array} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (let* ((t_0
         (* (pow (sqrt k) -1.0) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0)))))
   (if (<= t_0 5e-227)
     0.0
     (if (<= t_0 2e+153)
       (sqrt (* (/ (* n (PI)) k) 2.0))
       (/ (sqrt (+ n n)) (sqrt k))))))

Derivation

1. Split input into 3 regimes

2. if (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64)))) < 4.99999999999999961e-227

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   4. Applied rewrites 1.6%

      \[\leadsto \color{blue}{\frac{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}}} \]
   5. Step-by-step derivation

      1. lift-pow.f64 N/A

         \[\leadsto \frac{\color{blue}{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}}{\sqrt{k}} \]

      2. lift-*.f64 N/A

         \[\leadsto \frac{{\color{blue}{\left(0 \cdot n\right)}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      3. mul0-lft N/A

         \[\leadsto \frac{{\color{blue}{0}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      4. pow-base-0 98.0

         \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   6. Applied rewrites 98.0%

      \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   7. Taylor expanded in k around 0

      \[\leadsto \color{blue}{0} \]
   8. Step-by-step derivation

   9. Applied rewrites 98.0%

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

   if 4.99999999999999961e-227 < (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64)))) < 2e153

   1. Initial program 99.2%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around 0

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \cdot \sqrt{2}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      3. lower-sqrt.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      6. *-commutative N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      7. lower-*.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      8. lower-PI.f64 98.2

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot n}{k}} \]

   5. Applied rewrites 98.2%

      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{\mathsf{PI}\left(\right) \cdot n}{k}}} \]
   6. Step-by-step derivation

   7. Applied rewrites 98.6%

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k} \cdot 2}} \]

   if 2e153 < (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64))))

   1. Initial program 99.8%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around 0

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \cdot \sqrt{2}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      3. lower-sqrt.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      6. *-commutative N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      7. lower-*.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      8. lower-PI.f64 3.4

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot n}{k}} \]

   5. Applied rewrites 3.4%

      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{\mathsf{PI}\left(\right) \cdot n}{k}}} \]
   6. Step-by-step derivation

   7. Applied rewrites 38.2%

      \[\leadsto \frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\color{blue}{\sqrt{k}}} \]
   8. Step-by-step derivation

   9. Applied rewrites 8.5%

      \[\leadsto \frac{\sqrt{n + n}}{\sqrt{k}} \]
3. Recombined 3 regimes into one program.

4. Final simplification 59.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{elif}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 2 \cdot 10^{+153}:\\ \;\;\;\;\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k} \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{n + n}}{\sqrt{k}}\\ \end{array} \]
5. Add Preprocessing

Alternative 4: 73.7% accurate, 0.5× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\sqrt{k}}\\ \end{array} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (if (<=
      (* (pow (sqrt k) -1.0) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0)))
      5e-227)
   0.0
   (/ (sqrt (* (* n 2.0) (PI))) (sqrt k))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64)))) < 4.99999999999999961e-227

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   4. Applied rewrites 1.6%

      \[\leadsto \color{blue}{\frac{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}}} \]
   5. Step-by-step derivation

      1. lift-pow.f64 N/A

         \[\leadsto \frac{\color{blue}{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}}{\sqrt{k}} \]

      2. lift-*.f64 N/A

         \[\leadsto \frac{{\color{blue}{\left(0 \cdot n\right)}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      3. mul0-lft N/A

         \[\leadsto \frac{{\color{blue}{0}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      4. pow-base-0 98.0

         \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   6. Applied rewrites 98.0%

      \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   7. Taylor expanded in k around 0

      \[\leadsto \color{blue}{0} \]
   8. Step-by-step derivation

   9. Applied rewrites 98.0%

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

   if 4.99999999999999961e-227 < (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64))))

   1. Initial program 99.5%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around 0

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \cdot \sqrt{2}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      3. lower-sqrt.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      6. *-commutative N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      7. lower-*.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      8. lower-PI.f64 48.1

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot n}{k}} \]

   5. Applied rewrites 48.1%

      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{\mathsf{PI}\left(\right) \cdot n}{k}}} \]
   6. Step-by-step derivation

   7. Applied rewrites 66.4%

      \[\leadsto \frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\color{blue}{\sqrt{k}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 72.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\sqrt{k}}\\ \end{array} \]
5. Add Preprocessing

Alternative 5: 62.4% accurate, 0.5× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k} \cdot 2}\\ \end{array} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (if (<=
      (* (pow (sqrt k) -1.0) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0)))
      5e-227)
   0.0
   (sqrt (* (/ (* n (PI)) k) 2.0))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64)))) < 4.99999999999999961e-227

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   4. Applied rewrites 1.6%

      \[\leadsto \color{blue}{\frac{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}}} \]
   5. Step-by-step derivation

      1. lift-pow.f64 N/A

         \[\leadsto \frac{\color{blue}{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}}{\sqrt{k}} \]

      2. lift-*.f64 N/A

         \[\leadsto \frac{{\color{blue}{\left(0 \cdot n\right)}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      3. mul0-lft N/A

         \[\leadsto \frac{{\color{blue}{0}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      4. pow-base-0 98.0

         \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   6. Applied rewrites 98.0%

      \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   7. Taylor expanded in k around 0

      \[\leadsto \color{blue}{0} \]
   8. Step-by-step derivation

   9. Applied rewrites 98.0%

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

   if 4.99999999999999961e-227 < (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64))))

   1. Initial program 99.5%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around 0

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \cdot \sqrt{2}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      3. lower-sqrt.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      6. *-commutative N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      7. lower-*.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      8. lower-PI.f64 48.1

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot n}{k}} \]

   5. Applied rewrites 48.1%

      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{\mathsf{PI}\left(\right) \cdot n}{k}}} \]
   6. Step-by-step derivation

   7. Applied rewrites 48.2%

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k} \cdot 2}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 57.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k} \cdot 2}\\ \end{array} \]
5. Add Preprocessing

Alternative 6: 34.1% accurate, 0.6× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{n}{k} \cdot 2}\\ \end{array} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (if (<=
      (* (pow (sqrt k) -1.0) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0)))
      5e-227)
   0.0
   (sqrt (* (/ n k) 2.0))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64)))) < 4.99999999999999961e-227

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   4. Applied rewrites 1.6%

      \[\leadsto \color{blue}{\frac{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}}} \]
   5. Step-by-step derivation

      1. lift-pow.f64 N/A

         \[\leadsto \frac{\color{blue}{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}}{\sqrt{k}} \]

      2. lift-*.f64 N/A

         \[\leadsto \frac{{\color{blue}{\left(0 \cdot n\right)}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      3. mul0-lft N/A

         \[\leadsto \frac{{\color{blue}{0}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

      4. pow-base-0 98.0

         \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   6. Applied rewrites 98.0%

      \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

   7. Taylor expanded in k around 0

      \[\leadsto \color{blue}{0} \]
   8. Step-by-step derivation

   9. Applied rewrites 98.0%

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

   if 4.99999999999999961e-227 < (*.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 k)) (pow.f64 (*.f64 (*.f64 #s(literal 2 binary64) (PI.f64)) n) (/.f64 (-.f64 #s(literal 1 binary64) k) #s(literal 2 binary64))))

   1. Initial program 99.5%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around 0

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \cdot \sqrt{2}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      3. lower-sqrt.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      6. *-commutative N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      7. lower-*.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      8. lower-PI.f64 48.1

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot n}{k}} \]

   5. Applied rewrites 48.1%

      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{\mathsf{PI}\left(\right) \cdot n}{k}}} \]
   6. Step-by-step derivation

   7. Applied rewrites 66.4%

      \[\leadsto \frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\color{blue}{\sqrt{k}}} \]
   8. Step-by-step derivation

   9. Applied rewrites 10.8%

      \[\leadsto \color{blue}{\sqrt{\frac{n}{k} \cdot 2}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 26.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(\sqrt{k}\right)}^{-1} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \leq 5 \cdot 10^{-227}:\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\sqrt{\frac{n}{k} \cdot 2}\\ \end{array} \]
5. Add Preprocessing

Alternative 7: 99.5% accurate, 1.1× speedup

Math

\[\begin{array}{l} \\ \frac{{\left(\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}}{\sqrt{k}} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (/ (pow (* (* n 2.0) (PI)) (fma -0.5 k 0.5)) (sqrt k)))

Derivation

1. Initial program 99.6%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Add Preprocessing

3. Taylor expanded in k around inf

   \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{e^{\frac{1}{2} \cdot \left(\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(1 - k\right)\right)}} \]
4. Step-by-step derivation

   1. *-commutative N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot e^{\frac{1}{2} \cdot \color{blue}{\left(\left(1 - k\right) \cdot \log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)\right)}} \]

   2. associate-*r* N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot e^{\color{blue}{\left(\frac{1}{2} \cdot \left(1 - k\right)\right) \cdot \log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

   3. *-commutative N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot e^{\color{blue}{\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\frac{1}{2} \cdot \left(1 - k\right)\right)}} \]

   4. exp-prod N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{{\left(e^{\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)}} \]

   5. lower-pow.f64 N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{{\left(e^{\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)}} \]

   6. rem-exp-log N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot {\color{blue}{\left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

   7. associate-*r* N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot {\color{blue}{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

   8. lower-*.f64 N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot {\color{blue}{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

   9. lower-*.f64 N/A

      \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\color{blue}{\left(2 \cdot n\right)} \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

   10. lower-PI.f64 N/A

       \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

   11. *-lft-identity N/A

       \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \left(1 - \color{blue}{1 \cdot k}\right)\right)} \]

   12. metadata-eval N/A

       \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \left(1 - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot k\right)\right)} \]

   13. fp-cancel-sign-sub-inv N/A

       \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \color{blue}{\left(1 + -1 \cdot k\right)}\right)} \]

   14. +-commutative N/A

       \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \color{blue}{\left(-1 \cdot k + 1\right)}\right)} \]

   15. distribute-lft-in N/A

       \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\color{blue}{\left(\frac{1}{2} \cdot \left(-1 \cdot k\right) + \frac{1}{2} \cdot 1\right)}} \]

5. Applied rewrites 99.6%

   \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}} \]
6. Step-by-step derivation

   1. lift-*.f64 N/A

      \[\leadsto \color{blue}{\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)}} \]

   2. lift-/.f64 N/A

      \[\leadsto \color{blue}{\frac{1}{\sqrt{k}}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)} \]

   3. associate-*l/ N/A

      \[\leadsto \color{blue}{\frac{1 \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)}}{\sqrt{k}}} \]

   4. *-lft-identity N/A

      \[\leadsto \frac{\color{blue}{{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)}}}{\sqrt{k}} \]

   5. lower-/.f64 99.6

      \[\leadsto \color{blue}{\frac{{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}}{\sqrt{k}}} \]

7. Applied rewrites 99.6%

   \[\leadsto \color{blue}{\frac{{\left(\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}}{\sqrt{k}}} \]
8. Add Preprocessing

Alternative 8: 98.2% accurate, 1.1× speedup

Math

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;k \leq 0.0055:\\ \;\;\;\;\frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\sqrt{k}}\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(n + n\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}}{\sqrt{k}}\\ \end{array} \end{array} \]

FPCore

(FPCore (k n)
 :precision binary64
 (if (<= k 0.0055)
   (/ (sqrt (* (* n 2.0) (PI))) (sqrt k))
   (/ (pow (+ n n) (fma -0.5 k 0.5)) (sqrt k))))

Derivation

1. Split input into 2 regimes

2. if k < 0.0054999999999999997

   1. Initial program 99.3%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around 0

      \[\leadsto \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \cdot \sqrt{2}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      2. lower-*.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      3. lower-sqrt.f64 N/A

         \[\leadsto \color{blue}{\sqrt{2}} \cdot \sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}} \]

      4. lower-sqrt.f64 N/A

         \[\leadsto \sqrt{2} \cdot \color{blue}{\sqrt{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      5. lower-/.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{\frac{n \cdot \mathsf{PI}\left(\right)}{k}}} \]

      6. *-commutative N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      7. lower-*.f64 N/A

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right) \cdot n}}{k}} \]

      8. lower-PI.f64 71.6

         \[\leadsto \sqrt{2} \cdot \sqrt{\frac{\color{blue}{\mathsf{PI}\left(\right)} \cdot n}{k}} \]

   5. Applied rewrites 71.6%

      \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{\frac{\mathsf{PI}\left(\right) \cdot n}{k}}} \]
   6. Step-by-step derivation

   7. Applied rewrites 99.2%

      \[\leadsto \frac{\sqrt{\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)}}{\color{blue}{\sqrt{k}}} \]

   if 0.0054999999999999997 < k

   1. Initial program 100.0%

      \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
   2. Add Preprocessing

   3. Taylor expanded in k around inf

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{e^{\frac{1}{2} \cdot \left(\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(1 - k\right)\right)}} \]
   4. Step-by-step derivation

      1. *-commutative N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot e^{\frac{1}{2} \cdot \color{blue}{\left(\left(1 - k\right) \cdot \log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)\right)}} \]

      2. associate-*r* N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot e^{\color{blue}{\left(\frac{1}{2} \cdot \left(1 - k\right)\right) \cdot \log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}} \]

      3. *-commutative N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot e^{\color{blue}{\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right) \cdot \left(\frac{1}{2} \cdot \left(1 - k\right)\right)}} \]

      4. exp-prod N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{{\left(e^{\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)}} \]

      5. lower-pow.f64 N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{{\left(e^{\log \left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)}} \]

      6. rem-exp-log N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot {\color{blue}{\left(2 \cdot \left(n \cdot \mathsf{PI}\left(\right)\right)\right)}}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

      7. associate-*r* N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot {\color{blue}{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

      8. lower-*.f64 N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot {\color{blue}{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

      9. lower-*.f64 N/A

         \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\color{blue}{\left(2 \cdot n\right)} \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

      10. lower-PI.f64 N/A

          \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)}^{\left(\frac{1}{2} \cdot \left(1 - k\right)\right)} \]

      11. *-lft-identity N/A

          \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \left(1 - \color{blue}{1 \cdot k}\right)\right)} \]

      12. metadata-eval N/A

          \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \left(1 - \color{blue}{\left(\mathsf{neg}\left(-1\right)\right)} \cdot k\right)\right)} \]

      13. fp-cancel-sign-sub-inv N/A

          \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \color{blue}{\left(1 + -1 \cdot k\right)}\right)} \]

      14. +-commutative N/A

          \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\frac{1}{2} \cdot \color{blue}{\left(-1 \cdot k + 1\right)}\right)} \]

      15. distribute-lft-in N/A

          \[\leadsto \frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\color{blue}{\left(\frac{1}{2} \cdot \left(-1 \cdot k\right) + \frac{1}{2} \cdot 1\right)}} \]

   5. Applied rewrites 100.0%

      \[\leadsto \frac{1}{\sqrt{k}} \cdot \color{blue}{{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}} \]
   6. Step-by-step derivation

      1. lift-*.f64 N/A

         \[\leadsto \color{blue}{\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)}} \]

      2. lift-/.f64 N/A

         \[\leadsto \color{blue}{\frac{1}{\sqrt{k}}} \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)} \]

      3. associate-*l/ N/A

         \[\leadsto \color{blue}{\frac{1 \cdot {\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)}}{\sqrt{k}}} \]

      4. *-lft-identity N/A

         \[\leadsto \frac{\color{blue}{{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(\frac{-1}{2}, k, \frac{1}{2}\right)\right)}}}{\sqrt{k}} \]

      5. lower-/.f64 100.0

         \[\leadsto \color{blue}{\frac{{\left(\left(2 \cdot n\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}}{\sqrt{k}}} \]

   7. Applied rewrites 100.0%

      \[\leadsto \color{blue}{\frac{{\left(\left(n \cdot 2\right) \cdot \mathsf{PI}\left(\right)\right)}^{\left(\mathsf{fma}\left(-0.5, k, 0.5\right)\right)}}{\sqrt{k}}} \]
   8. Step-by-step derivation

   9. Applied rewrites 98.6%

      \[\leadsto \frac{{\left(n + n\right)}^{\left(\mathsf{fma}\left(\color{blue}{-0.5}, k, 0.5\right)\right)}}{\sqrt{k}} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 9: 27.5% accurate, 152.0× speedup

Math

\[\begin{array}{l} \\ 0 \end{array} \]

FPCore

(FPCore (k n) :precision binary64 0.0)

C

double code(double k, double n) {
	return 0.0;
}

Fortran

real(8) function code(k, n)
    real(8), intent (in) :: k
    real(8), intent (in) :: n
    code = 0.0d0
end function

Java

public static double code(double k, double n) {
	return 0.0;
}

Python

def code(k, n):
	return 0.0

Julia

function code(k, n)
	return 0.0
end

MATLAB

function tmp = code(k, n)
	tmp = 0.0;
end

Wolfram

code[k_, n_] := 0.0

Derivation

1. Initial program 99.6%

   \[\frac{1}{\sqrt{k}} \cdot {\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot n\right)}^{\left(\frac{1 - k}{2}\right)} \]
2. Add Preprocessing

4. Applied rewrites 29.1%

   \[\leadsto \color{blue}{\frac{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}}} \]
5. Step-by-step derivation

   1. lift-pow.f64 N/A

      \[\leadsto \frac{\color{blue}{{\left(0 \cdot n\right)}^{\left(\frac{1 - k}{8}\right)}}}{\sqrt{k}} \]

   2. lift-*.f64 N/A

      \[\leadsto \frac{{\color{blue}{\left(0 \cdot n\right)}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

   3. mul0-lft N/A

      \[\leadsto \frac{{\color{blue}{0}}^{\left(\frac{1 - k}{8}\right)}}{\sqrt{k}} \]

   4. pow-base-0 19.5

      \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

6. Applied rewrites 19.5%

   \[\leadsto \frac{\color{blue}{0}}{\sqrt{k}} \]

7. Taylor expanded in k around 0

   \[\leadsto \color{blue}{0} \]
8. Step-by-step derivation

9. Applied rewrites 19.5%

   \[\leadsto \color{blue}{0} \]
10. Add Preprocessing

Reproduce

herbie shell --seed 2024337 
(FPCore (k n)
  :name "Migdal et al, Equation (51)"
  :precision binary64
  (* (/ 1.0 (sqrt k)) (pow (* (* 2.0 (PI)) n) (/ (- 1.0 k) 2.0))))