		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))))))