		Search-engine friendly clone of the ACL2 documentation.

Sin-cos

Compute-series

Series approximation to SIN/COS.

This function is used to calculate the following Maclaurin series. To compute SIN:

x - \frac{x^3}{3!} + \frac{x^5}{5!} - \frac{x^7}{7!} + ...

To compute COS:

1- \frac{x^2}{2!} + \frac{x^4}{4!} - \frac{x^6}{6!} + ...

Arguments:

x -- x
parity -- T to add the new term, NIL to subtract the new term.
ex -- x^{num}
fact -- num!
itr -- Number of iterations
ans -- Accumulated answer.

Definitions and Theorems

Function: compute-series

(defun compute-series (x parity ex fact num itr ans)
  (declare (xargs :guard (and (rationalp x)
                              (booleanp parity)
                              (rationalp ex)
                              (integerp fact)
                              (> fact 0)
                              (integerp num)
                              (>= num 0)
                              (integerp itr)
                              (>= itr 0)
                              (rationalp ans))))
  (if (zp itr)
      ans
    (compute-series x (not parity)
                    (* x x ex)
                    (* (+ 2 num) (+ 1 num) fact)
                    (+ 2 num)
                    (1- itr)
                    (if parity (+ ans (/ ex fact))
                      (- ans (/ ex fact))))))