prodigy.analysis.lowerbounds.egcalc

Exact generating-function calculus over a fixed product denominator.

A (generalised) generating function is represented as P / D where D is a fixed product denominator:

D = (1 - r_1 X_1^{p_1}) * ... * (1 - r_k X_k^{p_k})       (r_i >= 0 rational, p_i >= 1; r_i = 0: no factor)

and P is a polynomial with rational coefficients, stored as a dict mapping exponent tuples to fractions.Fraction. The coefficients of P / D are eventually geometric: along variable i they satisfy c_{n + p_i e_i} = r_i c_n as soon as n_i exceeds the degree of P in X_i.

All loop-free pGCL statements of the supported fragment map numerators over D to numerators over the same D: guards and observations comparing a single variable with a constant (or testing it modulo m with m | p_i), increments and decrements (monus) by constants, constant assignments, sampling from unif, bernoulli and binomial (and from geometric(q) if r_i = 1 - q and p_i = 1), probabilistic choice, conditionals, observe (which removes the violating mass) and abort (divergence).

Coefficient-wise nonnegativity of P / D is decided exactly by finitely many coefficients (Lemma “finite positivity check” of the paper): P / D >= 0 iff all coefficients in the box prod_i [0, deg_i P + p_i - 1] are nonnegative.

class Denominator(rates, periods)[source]

Bases: object

The fixed product denominator prod_i (1 - r_i X_i^{p_i}).

Parameters:
value_at_one()[source]
Return type:

Fraction

factor(i)[source]

The factor 1 - r_i X_i^{p_i} as a numerator.

Parameters:

i (int)

Return type:

Dict[Tuple[int, ...], Fraction]

poly()[source]

D itself as a numerator (i.e. the generating function 1).

Return type:

Dict[Tuple[int, ...], Fraction]

without(i)[source]
Parameters:

i (int)

Return type:

Denominator

padd(*polys)[source]
Parameters:

polys (Dict[Tuple[int, ...], Fraction])

Return type:

Dict[Tuple[int, ...], Fraction]

pscale(poly, a)[source]
Parameters:

poly (Dict[Tuple[int, ...], Fraction])

Return type:

Dict[Tuple[int, ...], Fraction]

pmul(p1, p2)[source]
Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

pshift(poly, i, k)[source]

Multiply by X_i^k; k may be negative if all exponents stay nonnegative.

Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

degrees(poly, d)[source]
Parameters:
Return type:

List[int]

monomial(d, e, c=Fraction(1, 1))[source]
Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

class GFCalculus(variables, den)[source]

Bases: object

Exact transformer semantics of loop-free statements on numerators over a fixed denominator.

Parameters:
with_den(den)[source]
Parameters:

den (Denominator)

Return type:

GFCalculus

coeffs_along(poly, i, upto)[source]

The X_i-coefficients c_0..c_upto of P / D, each as a numerator over D without the X_i factor (exponent i set to 0).

Parameters:
Return type:

List[Dict[Tuple[int, ...], Fraction]]

restrict_pred(poly, i, pred, threshold, modulus)[source]

Restriction of P / D to the states whose i-th component satisfies pred, where pred(v) depends only on v mod modulus for v >= threshold; requires modulus | p_i if r_i != 0.

Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

eliminate(poly, i)[source]

F(X_i = 1) as a numerator over D without the X_i factor (exponent i set to 0), or None if the series diverges at X_i = 1 (only possible if r_i >= 1).

Parameters:
Return type:

Dict[Tuple[int, ...], Fraction] | None

restrict(poly, guard)[source]

Restriction <P/D>_guard of the measure to the states satisfying guard.

Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

run(stmt, poly)[source]

Forward semantics of a loop-free statement on the measure P / D (unnormalised; observe removes the violating mass, abort diverges).

Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

assign(var, e, poly)[source]
Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

decrement(poly, i, k)[source]

x_i := x_i - k with monus semantics (values below k become 0).

Parameters:
Return type:

Dict[Tuple[int, ...], Fraction]

expand(poly, box)[source]

The coefficients of P / D on the box prod_i [0, box_i] (object array of Fractions).

Parameters:
Return type:

ndarray

positivity_box(poly)[source]
Parameters:

poly (Dict[Tuple[int, ...], Fraction])

Return type:

List[int]

is_nonneg(poly)[source]

Exact decision of coefficient-wise nonnegativity of P / D.

Parameters:

poly (Dict[Tuple[int, ...], Fraction])

Return type:

bool

first_negative(poly)[source]

A coefficient of P / D that is negative (state and value), or None.

Parameters:

poly (Dict[Tuple[int, ...], Fraction])

Return type:

Tuple[Tuple[int, ...], Fraction] | None

coefficient(poly, state)[source]
Parameters:
Return type:

Fraction

mass(poly)[source]

Total mass (P / D)(1, ..., 1) in [0, inf] (exact); math.inf if the series diverges.

Parameters:

poly (Dict[Tuple[int, ...], Fraction])

Return type:

Fraction | float

moment(poly, i)[source]

First moment sum_n n_i * coeff_n(P / D) of variable i (exact), math.inf if it diverges. Requires P / D >= 0 for the value inf to be meaningful.

Parameters:
Return type:

Fraction | float

defect_mass(poly, sign=1)[source]

sum_n max(sign * coeff_n(P/D), 0) over all states (exact; inf if a growing tail is positive).

Parameters:
Return type:

Fraction | float

to_expr(poly)[source]

P / D as an expression string in the program variables (parsable by Prodigy’s factories).

Parameters:

poly (Dict[Tuple[int, ...], Fraction])

Return type:

str

directed_decimal(q, upward, digits=10)[source]

Decimal string with digits significant digits rounded towards +inf (upward) or -inf.

Parameters:
Return type:

str