		Search-engine friendly clone of the ACL2 documentation.

Sin-cos

Fast-compute-series

Efficient 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!} + ...

Rather than accumulating each term as shown, we instead compute the numerator and denominator of the sum, and return these two values. This avoids the necessity of reducing each rational as it is accumulated. On one set of examples this procudure was almost an order of magnitude faster than the simple summation given by compute-series.

Given x^2 as \frac{num-x^2}{denom-x^2}, and a partial sum \frac{num-sum}{denom-sum}, we compute the next partial sum as:

\frac{num-sum}{denom-sum}
   *
\frac{
   denom-x^2 (n + 1) (n + 2)
}{ denom-x^2 (n + 1) (n + 2) }
  *
\frac{
    num-x^n num-x^2
}{  denom-x^2 (n + 1) (n + 2)  }

Again, the rationals are not actually computed, and instead we simply return the numerator and denominator of the answer.

Arguments:

num-x^2 -- (Numerator of x)^2.
denom-x^2 -- (Denominator of x)^2.
num-x^n -- (num-x)^n
num-sum -- Numerator of partial sum.
denom-sum -- Denominator of partial sum.
n -- n
parity -- T to add next term, NIL to subtract next term.
itr -- Number of iterations to perform.

Definitions and Theorems

Function: fast-compute-series

(defun fast-compute-series
       (num-x^2 denom-x^2
                num-x^n num-sum denom-sum n parity itr)
  (declare (xargs :guard (and (integerp num-x^2)
                              (integerp denom-x^2)
                              (not (= denom-x^2 0))
                              (integerp num-x^n)
                              (integerp num-sum)
                              (integerp denom-sum)
                              (not (= denom-sum 0))
                              (integerp n)
                              (<= 0 n)
                              (booleanp parity)
                              (integerp itr)
                              (<= 0 itr))))
  (if (zp itr)
      (mv num-sum denom-sum)
    (let* ((n+1*n+2 (* (+ n 1) (+ n 2)))
           (multiplier (* denom-x^2 n+1*n+2))
           (new-denom-sum (* denom-sum multiplier))
           (adjusted-num-sum (* num-sum multiplier))
           (new-num-x^n (* num-x^n num-x^2))
           (new-num-sum (if parity (+ adjusted-num-sum new-num-x^n)
                          (- adjusted-num-sum new-num-x^n))))
      (fast-compute-series num-x^2 denom-x^2 new-num-x^n
                           new-num-sum new-denom-sum (+ 2 n)
                           (not parity)
                           (1- itr)))))