2 * cos ( 2* (i+1) -1 * PI / (2*n))

Percentage Accurate: 96.2% → 99.0%
Time: 6.0s
Alternatives: 7
Speedup: 1.1×

Specification

?
\[\left(2 \leq i \land i \leq 16\right) \land \left(2 \leq n \land n \leq 16\right)\]
\[\begin{array}{l} \\ 2 \cdot \cos \left(2 \cdot \left(i + 1\right) - \frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right) \end{array} \]
(FPCore (i n)
 :precision binary64
 (* 2.0 (cos (- (* 2.0 (+ i 1.0)) (/ (* 1.0 (PI)) (* 2.0 n))))))
\begin{array}{l}

\\
2 \cdot \cos \left(2 \cdot \left(i + 1\right) - \frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right)
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 7 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 96.2% accurate, 1.0× speedup?

\[\begin{array}{l} \\ 2 \cdot \cos \left(2 \cdot \left(i + 1\right) - \frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right) \end{array} \]
(FPCore (i n)
 :precision binary64
 (* 2.0 (cos (- (* 2.0 (+ i 1.0)) (/ (* 1.0 (PI)) (* 2.0 n))))))
\begin{array}{l}

\\
2 \cdot \cos \left(2 \cdot \left(i + 1\right) - \frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right)
\end{array}

Alternative 1: 99.0% accurate, 0.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \frac{\mathsf{PI}\left(\right)}{n}\\ 2 \cdot \left(\cos \left(i \cdot 2\right) \cdot \mathsf{fma}\left(\cos \left(t\_0 \cdot -0.5\right), \cos 2, \sin 2 \cdot \sin \left(t\_0 \cdot 0.5\right)\right) - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \end{array} \end{array} \]
(FPCore (i n)
 :precision binary64
 (let* ((t_0 (/ (PI) n)))
   (*
    2.0
    (-
     (*
      (cos (* i 2.0))
      (fma (cos (* t_0 -0.5)) (cos 2.0) (* (sin 2.0) (sin (* t_0 0.5)))))
     (* (sin (* i 2.0)) (sin (- 2.0 (/ (PI) (* n 2.0)))))))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \frac{\mathsf{PI}\left(\right)}{n}\\
2 \cdot \left(\cos \left(i \cdot 2\right) \cdot \mathsf{fma}\left(\cos \left(t\_0 \cdot -0.5\right), \cos 2, \sin 2 \cdot \sin \left(t\_0 \cdot 0.5\right)\right) - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)
\end{array}
\end{array}
Derivation

  1. Initial program 96.4%

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

    1. lift-cos.f64N/A

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

    2. lift--.f64N/A

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

    3. lift-*.f64N/A

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

    4. lift-+.f64N/A

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

    5. distribute-rgt-inN/A

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

    6. metadata-evalN/A

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

    7. associate--l+N/A

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

    8. cos-sumN/A

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

    9. lower--.f64N/A

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

  4. Applied rewrites98.7%

    \[\leadsto 2 \cdot \color{blue}{\left(\cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} \]
  5. Step-by-step derivation

    1. lift-cos.f64N/A

      \[\leadsto 2 \cdot \left(\cos \left(i \cdot 2\right) \cdot \color{blue}{\cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)} - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \]

    2. lift--.f64N/A

      \[\leadsto 2 \cdot \left(\cos \left(i \cdot 2\right) \cdot \cos \color{blue}{\left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)} - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \]

    3. cos-diffN/A

      \[\leadsto 2 \cdot \left(\cos \left(i \cdot 2\right) \cdot \color{blue}{\left(\cos 2 \cdot \cos \left(\frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) + \sin 2 \cdot \sin \left(\frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \]

  6. Applied rewrites99.0%

    \[\leadsto 2 \cdot \left(\cos \left(i \cdot 2\right) \cdot \color{blue}{\mathsf{fma}\left(\cos \left(\frac{\mathsf{PI}\left(\right)}{n} \cdot -0.5\right), \cos 2, \sin 2 \cdot \sin \left(\frac{\mathsf{PI}\left(\right)}{n} \cdot 0.5\right)\right)} - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \]
  7. Add Preprocessing

Alternative 2: 98.8% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\\ 2 \cdot \mathsf{fma}\left(\sin t\_0, -\sin \left(2 \cdot i\right), \cos t\_0 \cdot \cos \left(2 \cdot i\right)\right) \end{array} \end{array} \]
(FPCore (i n)
 :precision binary64
 (let* ((t_0 (fma (/ (PI) n) -0.5 2.0)))
   (* 2.0 (fma (sin t_0) (- (sin (* 2.0 i))) (* (cos t_0) (cos (* 2.0 i)))))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\\
2 \cdot \mathsf{fma}\left(\sin t\_0, -\sin \left(2 \cdot i\right), \cos t\_0 \cdot \cos \left(2 \cdot i\right)\right)
\end{array}
\end{array}
Derivation

  1. Initial program 96.4%

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

    1. lift-cos.f64N/A

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

    2. lift--.f64N/A

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

    3. lift-*.f64N/A

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

    4. lift-+.f64N/A

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

    5. distribute-rgt-inN/A

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

    6. metadata-evalN/A

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

    7. associate--l+N/A

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

    8. cos-sumN/A

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

    9. lower--.f64N/A

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

  4. Applied rewrites98.7%

    \[\leadsto 2 \cdot \color{blue}{\left(\cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} \]
  5. Step-by-step derivation

    1. lift--.f64N/A

      \[\leadsto 2 \cdot \color{blue}{\left(\cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} \]

    2. sub-negN/A

      \[\leadsto 2 \cdot \color{blue}{\left(\cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) + \left(\mathsf{neg}\left(\sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)\right)\right)} \]

    3. +-commutativeN/A

      \[\leadsto 2 \cdot \color{blue}{\left(\left(\mathsf{neg}\left(\sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)\right) + \cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} \]

    4. lift-*.f64N/A

      \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)}\right)\right) + \cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \]

    5. *-commutativeN/A

      \[\leadsto 2 \cdot \left(\left(\mathsf{neg}\left(\color{blue}{\sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) \cdot \sin \left(i \cdot 2\right)}\right)\right) + \cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \]

    6. distribute-rgt-neg-inN/A

      \[\leadsto 2 \cdot \left(\color{blue}{\sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) \cdot \left(\mathsf{neg}\left(\sin \left(i \cdot 2\right)\right)\right)} + \cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right) \]

    7. lower-fma.f64N/A

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(\sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right), \mathsf{neg}\left(\sin \left(i \cdot 2\right)\right), \cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} \]

  6. Applied rewrites98.8%

    \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(\sin \left(\mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\right), -\sin \left(2 \cdot i\right), \cos \left(\mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\right) \cdot \cos \left(2 \cdot i\right)\right)} \]
  7. Add Preprocessing

Alternative 3: 98.7% accurate, 0.3× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\\ 2 \cdot \left(\cos t\_0 \cdot \cos \left(2 \cdot i\right) - \sin t\_0 \cdot \sin \left(2 \cdot i\right)\right) \end{array} \end{array} \]
(FPCore (i n)
 :precision binary64
 (let* ((t_0 (fma (/ (PI) n) -0.5 2.0)))
   (* 2.0 (- (* (cos t_0) (cos (* 2.0 i))) (* (sin t_0) (sin (* 2.0 i)))))))
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\\
2 \cdot \left(\cos t\_0 \cdot \cos \left(2 \cdot i\right) - \sin t\_0 \cdot \sin \left(2 \cdot i\right)\right)
\end{array}
\end{array}
Derivation

  1. Initial program 96.4%

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

    1. lift-cos.f64N/A

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

    2. lift--.f64N/A

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

    3. lift-*.f64N/A

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

    4. lift-+.f64N/A

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

    5. distribute-rgt-inN/A

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

    6. metadata-evalN/A

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

    7. associate--l+N/A

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

    8. cos-sumN/A

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

    9. lower--.f64N/A

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

  4. Applied rewrites98.7%

    \[\leadsto 2 \cdot \color{blue}{\left(\cos \left(i \cdot 2\right) \cdot \cos \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) - \sin \left(i \cdot 2\right) \cdot \sin \left(2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} \]
  5. Step-by-step derivation

    1. Applied rewrites98.7%

      \[\leadsto 2 \cdot \color{blue}{\left(\cos \left(\mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\right) \cdot \cos \left(2 \cdot i\right) - \sin \left(\mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\right) \cdot \sin \left(2 \cdot i\right)\right)} \]
    2. Add Preprocessing

    Alternative 4: 98.5% accurate, 0.3× speedup?

    \[\begin{array}{l} \\ 2 \cdot \mathsf{fma}\left(\cos \left(\mathsf{fma}\left(i, 2, 2\right)\right), \cos \left(-0.5 \cdot \frac{\mathsf{PI}\left(\right)}{n}\right), \sin \left(\frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) \cdot \sin \left(\mathsf{fma}\left(i, 2, 2\right)\right)\right) \end{array} \]
    (FPCore (i n)
 :precision binary64
 (*
  2.0
  (fma
   (cos (fma i 2.0 2.0))
   (cos (* -0.5 (/ (PI) n)))
   (* (sin (/ (PI) (* n 2.0))) (sin (fma i 2.0 2.0))))))
    \begin{array}{l}

\\
2 \cdot \mathsf{fma}\left(\cos \left(\mathsf{fma}\left(i, 2, 2\right)\right), \cos \left(-0.5 \cdot \frac{\mathsf{PI}\left(\right)}{n}\right), \sin \left(\frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) \cdot \sin \left(\mathsf{fma}\left(i, 2, 2\right)\right)\right)
\end{array}
    Derivation

    1. Initial program 96.4%

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

      1. lift-cos.f64N/A

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

      2. lift--.f64N/A

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

      3. cos-diffN/A

        \[\leadsto 2 \cdot \color{blue}{\left(\cos \left(2 \cdot \left(i + 1\right)\right) \cdot \cos \left(\frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right) + \sin \left(2 \cdot \left(i + 1\right)\right) \cdot \sin \left(\frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right)\right)} \]

      4. lower-fma.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(\cos \left(2 \cdot \left(i + 1\right)\right), \cos \left(\frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right), \sin \left(2 \cdot \left(i + 1\right)\right) \cdot \sin \left(\frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right)\right)} \]

    4. Applied rewrites98.5%

      \[\leadsto 2 \cdot \color{blue}{\mathsf{fma}\left(\cos \left(\mathsf{fma}\left(i, 2, 2\right)\right), \cos \left(-0.5 \cdot \frac{\mathsf{PI}\left(\right)}{n}\right), \sin \left(\frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right) \cdot \sin \left(\mathsf{fma}\left(i, 2, 2\right)\right)\right)} \]
    5. Add Preprocessing

    Alternative 5: 96.4% accurate, 1.1× speedup?

    \[\begin{array}{l} \\ 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\right)\right) \end{array} \]
    (FPCore (i n)
 :precision binary64
 (* 2.0 (cos (fma i 2.0 (fma (/ (PI) n) -0.5 2.0)))))
    \begin{array}{l}

\\
2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)\right)\right)
\end{array}
    Derivation

    1. Initial program 96.4%

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

      1. lift--.f64N/A

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

      2. lift-*.f64N/A

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

      3. lift-+.f64N/A

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

      4. distribute-rgt-inN/A

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

      5. metadata-evalN/A

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

      6. associate--l+N/A

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

      7. lower-fma.f64N/A

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

      8. lower--.f6496.6

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

      9. lift-*.f64N/A

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

      10. *-lft-identity96.6

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \frac{\color{blue}{\mathsf{PI}\left(\right)}}{2 \cdot n}\right)\right) \]

      11. lift-*.f64N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \frac{\mathsf{PI}\left(\right)}{\color{blue}{2 \cdot n}}\right)\right) \]

      12. *-commutativeN/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \frac{\mathsf{PI}\left(\right)}{\color{blue}{n \cdot 2}}\right)\right) \]

      13. lower-*.f6496.6

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \frac{\mathsf{PI}\left(\right)}{\color{blue}{n \cdot 2}}\right)\right) \]

    4. Applied rewrites96.6%

      \[\leadsto 2 \cdot \cos \color{blue}{\left(\mathsf{fma}\left(i, 2, 2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}\right)\right)} \]
    5. Step-by-step derivation

      1. lift--.f64N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \color{blue}{2 - \frac{\mathsf{PI}\left(\right)}{n \cdot 2}}\right)\right) \]

      2. lift-/.f64N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \color{blue}{\frac{\mathsf{PI}\left(\right)}{n \cdot 2}}\right)\right) \]

      3. lift-*.f64N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \frac{\mathsf{PI}\left(\right)}{\color{blue}{n \cdot 2}}\right)\right) \]

      4. associate-/r*N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \color{blue}{\frac{\frac{\mathsf{PI}\left(\right)}{n}}{2}}\right)\right) \]

      5. lift-/.f64N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 - \frac{\color{blue}{\frac{\mathsf{PI}\left(\right)}{n}}}{2}\right)\right) \]

      6. div-invN/A

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

      7. metadata-evalN/A

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

      8. *-commutativeN/A

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

      9. cancel-sign-sub-invN/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \color{blue}{2 + \left(\mathsf{neg}\left(\frac{1}{2}\right)\right) \cdot \frac{\mathsf{PI}\left(\right)}{n}}\right)\right) \]

      10. metadata-evalN/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 + \color{blue}{\frac{-1}{2}} \cdot \frac{\mathsf{PI}\left(\right)}{n}\right)\right) \]

      11. lift-*.f64N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, 2 + \color{blue}{\frac{-1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{n}}\right)\right) \]

      12. +-commutativeN/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \color{blue}{\frac{-1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{n} + 2}\right)\right) \]

      13. lift-*.f64N/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \color{blue}{\frac{-1}{2} \cdot \frac{\mathsf{PI}\left(\right)}{n}} + 2\right)\right) \]

      14. *-commutativeN/A

        \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \color{blue}{\frac{\mathsf{PI}\left(\right)}{n} \cdot \frac{-1}{2}} + 2\right)\right) \]

      15. lower-fma.f6496.6

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

    6. Applied rewrites96.6%

      \[\leadsto 2 \cdot \cos \left(\mathsf{fma}\left(i, 2, \color{blue}{\mathsf{fma}\left(\frac{\mathsf{PI}\left(\right)}{n}, -0.5, 2\right)}\right)\right) \]
    7. Add Preprocessing

    Alternative 6: 19.5% accurate, 1.2× speedup?

    \[\begin{array}{l} \\ 2 \cdot \cos \left(\mathsf{fma}\left(2, i, 2\right)\right) \end{array} \]
    (FPCore (i n) :precision binary64 (* 2.0 (cos (fma 2.0 i 2.0))))
    double code(double i, double n) {
	return 2.0 * cos(fma(2.0, i, 2.0));
}

    function code(i, n)
	return Float64(2.0 * cos(fma(2.0, i, 2.0)))
end

    code[i_, n_] := N[(2.0 * N[Cos[N[(2.0 * i + 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

    \begin{array}{l}

\\
2 \cdot \cos \left(\mathsf{fma}\left(2, i, 2\right)\right)
\end{array}
    Derivation

    1. Initial program 96.4%

      \[2 \cdot \cos \left(2 \cdot \left(i + 1\right) - \frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right) \]
    2. Add Preprocessing

    3. Taylor expanded in n around inf

      \[\leadsto 2 \cdot \cos \color{blue}{\left(2 \cdot \left(1 + i\right)\right)} \]
    4. Step-by-step derivation

      1. distribute-lft-inN/A

        \[\leadsto 2 \cdot \cos \color{blue}{\left(2 \cdot 1 + 2 \cdot i\right)} \]

      2. metadata-evalN/A

        \[\leadsto 2 \cdot \cos \left(\color{blue}{2} + 2 \cdot i\right) \]

      3. +-commutativeN/A

        \[\leadsto 2 \cdot \cos \color{blue}{\left(2 \cdot i + 2\right)} \]

      4. lower-fma.f6419.4

        \[\leadsto 2 \cdot \cos \color{blue}{\left(\mathsf{fma}\left(2, i, 2\right)\right)} \]

    5. Applied rewrites19.4%

      \[\leadsto 2 \cdot \cos \color{blue}{\left(\mathsf{fma}\left(2, i, 2\right)\right)} \]
    6. Add Preprocessing

    Alternative 7: 9.4% accurate, 1.2× speedup?

    \[\begin{array}{l} \\ 2 \cdot \cos \left(2 \cdot i\right) \end{array} \]
    (FPCore (i n) :precision binary64 (* 2.0 (cos (* 2.0 i))))
    double code(double i, double n) {
	return 2.0 * cos((2.0 * i));
}

    real(8) function code(i, n)
    real(8), intent (in) :: i
    real(8), intent (in) :: n
    code = 2.0d0 * cos((2.0d0 * i))
end function

    public static double code(double i, double n) {
	return 2.0 * Math.cos((2.0 * i));
}

    def code(i, n):
	return 2.0 * math.cos((2.0 * i))

    function code(i, n)
	return Float64(2.0 * cos(Float64(2.0 * i)))
end

    function tmp = code(i, n)
	tmp = 2.0 * cos((2.0 * i));
end

    code[i_, n_] := N[(2.0 * N[Cos[N[(2.0 * i), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

    \begin{array}{l}

\\
2 \cdot \cos \left(2 \cdot i\right)
\end{array}
    Derivation

    1. Initial program 96.4%

      \[2 \cdot \cos \left(2 \cdot \left(i + 1\right) - \frac{1 \cdot \mathsf{PI}\left(\right)}{2 \cdot n}\right) \]
    2. Add Preprocessing

    3. Taylor expanded in i around inf

      \[\leadsto 2 \cdot \cos \color{blue}{\left(2 \cdot i\right)} \]
    4. Step-by-step derivation

      1. lower-*.f649.2

        \[\leadsto 2 \cdot \cos \color{blue}{\left(2 \cdot i\right)} \]

    5. Applied rewrites9.2%

      \[\leadsto 2 \cdot \cos \color{blue}{\left(2 \cdot i\right)} \]
    6. Add Preprocessing

    Reproduce

    ?
    herbie shell --seed 1 
(FPCore (i n)
  :name "2 * cos ( 2* (i+1) -1  * PI / (2*n))"
  :precision binary64
  :pre (and (and (<= 2.0 i) (<= i 16.0)) (and (<= 2.0 n) (<= n 16.0)))
  (* 2.0 (cos (- (* 2.0 (+ i 1.0)) (/ (* 1.0 (PI)) (* 2.0 n))))))