pub struct Count { /* private fields */ }Expand description
Closed-form sum of a Poly over given bounds. Counts can themselves be summed, since they are represented by a Poly divided by a constant.
Given the code:
for i from 0 to N:
for j from 0 to i^2:
yield 1The inner for body yields $1$ time, outer for body yields $\sum_{j=0}^{i^2-1} 1 = i^2$ times, and the full program yields $\sum_{i=0}^{N-1} i^2 = N(N-1)(2N - 1)/6$ times.
To count yields in general, we need an algorithm to count lattice points over Poly bounds. Treating other Vars as constants, and summing each term independently, the problem reduces to
$\sum_{x=0}^{P-1} x^{n}$ for variable $x$, constant $n$, and polynomial $P$.
We can convert to falling factorials $x_{(k)} = (x)(x-1)(x-2)\dots(x-k+1)$ using Stirling numbers of the second kind and the identity
$$x^{n} = \sum_{k=0}^n {S(n, k)} x_{(k)}$$
Therefore, $$\sum_{x=0}^{P-1} x^n = \sum_{x=0}^{P-1} \left( \sum_{k=0}^n S(n, k) x_{(k)} \right)$$
After the inner sum is expanded, each term will be a falling factorial that can be evaluated with the discrete power rule
$$\sum_{x=0}^{K-1} x_{(k)} = \frac{K_{(k+1)}}{k+1}$$
For example, in the case above, $P=N$ and $n=2$, so $$\sum_{x=0}^{N-1} x^2 = \sum_{x=0}^{N-1} \left( \sum_{k=0}^2 \textcolor{blue}{S(2, k)} \textcolor{red}{x_{(k)}} \right)$$ $$= \textcolor{blue}{0}\sum_{x=0}^{N-1} \textcolor{red}{x_{(0)}} + \textcolor{blue}{1}\sum_{x=0}^{N-1} \textcolor{red}{x_{(1)}} + \textcolor{blue}{1}\sum_{x=0}^{N-1} \textcolor{red}{x_{(2)}}$$ $$= \frac{N_{(2)}}{2} + \frac{N_{(3)}}{3}$$ $$= \frac{N(N-1)}{2} + \frac{N(N-1)(N-2)}{3}$$ $$= \frac{3(N^2-N) + 2(N^3-3N^2+2N)}{6}$$ $$= \frac{2N^3 - 3N^2 + N}{6}$$ $$= \frac{N(N−1)(2N−1)}{6}$$
This algorithm is implemented in Count::sum_below:
use sirius::solver::{poly::poly, count::Count};
let i2 = Count::ratio(poly!(i^2), 1);
let sum = i2.sum_below('i', &poly!(N));
assert_eq!(sum, Count::ratio(poly!(2*N^3 - 3*N^2 + N), 6));