Efficient Synthesis of Tight Polynomial Upper-Bounds for Systems of Conditional Polynomial Recurrences

Recurrence Relations. A recurrence relation is any equation expressing the n-th element of a sequence in terms of its previous elements. A system of recurrence relations is a family of recurrence relations for multiple sequences, where the n-th element of each sequence is expressed in terms of previous elements of not only that sequence, but also the other sequences in the family. For example, consider the following system: \(x_n = 2 \cdot x_{n-1} + y_{n-1} \wedge y_n = x_{n-1} + 2 \cdot y_{n-1}.\) This is an example of a system of linear recurrences, since each element is a linear combination of previous elements.

Recurrence Relations for Runtime Analysis. Recurrence relations are the most classical and standard formalism to capture the worst-case runtime behavior of recursive or divide-and-conquer algorithms with respect to the size n of their input [38]. When analyzing the asymptotic worst-case runtime of a recursive algorithm, the goal is to obtain an asymptotic upper-bound on the value of the n-th term of the recurrence. The two classical approaches here are the master theorem (MT) and the Akra-Bazzi method (AB).

Master Theorem (MT). First introduced in 1980 [12], the master theorem considers recurrences of the form \(\textstyle T(n) = a \cdot T\left( {n}/{b}\right) + f(n)\) and provides a recipe-like formula for an asymptotic solution in several cases with respect to a, b and f. For example, the solution is \(O(n^{\log _b a})\) when \(f(n) \in O(n^{\log _b a - \epsilon })\) for some \(\epsilon > 0\) and \(O(n^{\log _b a} \cdot \log n)\) when \(f(n) \in \varTheta (n^{\log _b a}).\) Given its ability to easily obtain bounds on the runtime of many common algorithms, MT is often included in undergraduate algorithms courses and textbooks [38].

Akra-Bazzi Method (AB). A significant limitation in MT is that it can only handle divide-and-conquer algorithms in which every instance is divided into a fixed number a of sub-instances of the same size n/b. The Akra-Bazzi method [1] extends MT by allowing sub-instances of differing sizes. Specifically, it handles recurrences of the formin which

For such recurrences, AB first finds a value p such that \(\sum _{i=1}^k a_i \cdot b_i^p = 1\) and then proves the asymptotic upper-boundBoth MT and AB can only handle linear recurrences.

Recurrence Solving in Static Analysis. Recurrence relations are also utilized as a way to summarize loops [47, 70, 75] and generate invariants [15, 72, 74]. Invariant generation is an essential first step in a wide variety of static program analyses [64, 76, 85]. Similarly, loop summarization enables the application of powerful methods such as algebraic [31, 34, 71] and Newtonian [45, 84] program analysis. A crucial difference between this kind of recurrence solving and the one in MT/AB is that worst-case runtime analysis aims to obtain an upper-bound on the n-th element T(n) of the recurrence. This upper-bound is often asymptotic, i.e. ignoring constant factors. In contrast, loop summarization and invariant generation methods need an exact closed-form formula for the n-th element. This leads to a harder problem, especially since the recurrence might not have a closed-form solution, and thus the tradeoff for these approaches is that they often handle a more restricted family of recurrences. In this work, we follow MT and AB and focus on finding upper-bounds, but our upper-bounds are not asymptotic and do not ignore constant factors.

Systems of Recurrences. A major limitation in AB and MT is that they can only handle a single recurrence relation. However, it is easy and natural to write programs consisting of several procedures with non-trivial recursive calls between them. In these cases, we will have several sequences \(T_1, T_2, \ldots , T_k,\) each corresponding to the runtime of one of the procedures, and the n-th element in each of them can depend on previous elements in the other sequences, as well.

Multi-variate Recurrences. Another limitation of MT and AB is that they only consider recurrences with a single variable n,  which is intuitively a measure of the size of the instance passed to the underlying recursive algorithm. However, there are many cases in which the size of an instance is not adequately captured by a single parameter. For example, the runtime of an algorithm that works with graphs is often dependent on both the number of vertices \(\vert V\vert \) and the number of edges \(\vert E \vert \) in the input graph. If we simply merge the two and define \(n := \vert V \vert + \vert E \vert ,\) this might lead to a gross over-approximation of the actual worst-case runtime of the algorithm. Indeed, the entire field of parameterized algorithms and complexity [39, 44] is based on studying the worst-case runtime of algorithms using more than one parameter. In such cases, MT and AB are not applicable and the runtimes are analyzed manually.

Conditional Recurrence Relations. A further challenge in solving recurrences is that many applications lead to so-called conditional recurrence relations [91]. These are recurrences in which there is no fixed formula for each element of the sequence, but we instead have several formulas and different conditions for the application of each. As a simple example, we might have two parameters n and m and different formulas for T(n, m) depending on whether n is larger than m or not. In such cases, neither AB nor MT can be applied. The state-of-the-art for conditional recurrences is [91] which can only handle periodic linear recurrences.

Probabilistic Recurrence Relations. Another related family of works are those that consider probabilistic recurrence relations, thus bounding the expected runtime of a randomized recursive algorithm such as Quick Sort or the probability that its runtime exceeds a certain threshold. In their setting, the size of the sub-instances is not necessarily deterministic but can instead be probabilistic. However, the number of sub-instances is fixed. For example, Quick Sort breaks down an array of size n into two arrays of size i and \(n-i-1,\) where each value of i is equally likely. The standard approach in this area is known as Karp’s cookbook [68, 69]. and resembles MT. Extensions of Karp’s cookbook include [35, 89, 90].

Our Contribution. In this work, we define an expressive class of recurrences called Generalized Polynomial Recurrence Systems (GPRS). Our GPRS setting is more expressive than that of MT and AB in the following dimensions:

We present the following results based on GPRS:

In short, we provide automated sound and complete algorithms that, for any fixed degree of the templates, can find the tightest polynomial bound for a given GPRS by means of a reduction to LP/SDP. As argued above, our setting is more general than the classical methods of MT and AB in several dimensions. We also provide an extensive set of illustrative examples, showcasing that our approach is applicable to recurrence relations that cannot be handled by MT or AB.

Limitations. The main limitation of our approach is that it requires everything to be polynomial. More specifically, all parts of the input GPRS, as well as the synthesized upper-bound have to be polynomial. This is a natural and inherent limitation due to our dependence on theorems in real algebraic geometry, which is the study of systems of polynomials and their real solutions. This being said, we can still apply the classical techniques of polynomial substitution and logarithmic substitution [38], to obtain exponential bounds such as \(3^n\) or bounds that have rational non-integral degrees, such as \(n^{2.83}\). We provide examples of such bounds in Sections 6 and 7. Moreover, we focus on the problem of solving systems of recurrence relations and do not consider how the system was obtained in the first place. This is natural in our main use-case, i.e. worst-case runtime analysis of algorithms, in which there is no implementation of the algorithm and instead the algorithm designer manually finds the recurrences and uses them to analyze asymptotic/exact runtimes [48]. In comparison, there are several previous works, such as [15, 65, 70], that extract systems of recurrences from programs. For such scenarios, our algorithm can only be applied to find the tightest possible polynomial bound of a given degree after the system of recurrences is generated by a separate tool.

Stellensatz-based Program Analysis. Our approach is a template-based algorithm using Farkas’ Lemma, Handelman’s Theorem and Putinar’s Positivstellensatz. These three theorems are classical and well-known results in polyhedral and real algebraic geometry. They have also been used in several previous works in static analysis, especially for invariant generation [26, 36], quantifier elimination [3], LTL model-checking [29] and program synthesis [2, 50]. These works reduce the respective static analysis problems to Quadratically-Constrained Quadratic Programming (QCQP) and rely on the Real Nullstellensatz for their completeness. In contrast, we do not use the Nullstellensatz and our reduction is to Linear Programming (LP) or Semi-definite Programming (SDP). QCQP is an NP-hard problem whereas both LP and SDP have PTIME solutions. Thus, for any fixed degree of template polynomials, our approach takes polynomial time. This indicates that, unsurprisingly, template-based recurrence solving is an easier problem in terms of complexity than both invariant generation and program synthesis. Similar approaches have also been used in the context of termination analysis, e.g. for the synthesis of ranking functions and ranking supermartingales [23‐25, 27, 28, 32, 63, 82, 93]. For any fixed degree of template polynomials, if tight program invariants are given as part of the input, then these approaches find ranking functions/supermartingales in PTIME. However, generating the required invariants themselves is not PTIME as mentioned above. We also remark that our algorithms do not depend on invariants or any input other than the system of recurrences.

Other Recurrence Solving Approaches. The closest previous work is a template-based recurrence solving approach and tool called CHORA [15], which builds upon [47]. In our experiments (Section 7), the outputs of the two approaches often coincide. However, in contrast to our approach, CHORA does not provide any completeness guarantees. Thus, there are instances in which our approach is able to synthesize a bound but CHORA fails. There are also instances in which our approach’s polynomial bound is tighter than CHORA’s. On the other hand, CHORA’s setting is more general since we focus only on polynomial templates and solutions, whereas CHORA creates templates in which arbitrary functions can serve as unknowns. For example, it is able to find a non-polynomial bound of \(O(n \cdot \lg n)\) for merge sort. Therefore, neither approach is subsumed by the other. A recent related work is [40], which also focuses on generality, i.e. being able to soundly synthesize bounds of different forms, rather than completeness for a particular type of bound. It takes a program as input and applies abstractions to enable the application of algebraic program analysis [30, 33, 37, 71] and methods for generating all polynomial invariants. Note that, as mentioned above, this is a strictly harder problem than the one considered in our setting. Another related work is [70], which automatically infers recurrences from programs and then provides a highly efficient compositional method to solve them. This method is efficient but not complete. An interesting direction of future work would be to combine [70] with our approach, i.e. first use [70] to obtain recurrence systems from programs and then use a combination of our complete method for polynomial bounds and [70]’s method for non-polynomial bounds to solve the resulting recurrences. Finally, there are many recurrence-solving methods developed as subroutines in the context of automated (amortized) resource analysis [7, 16, 17, 19‐22, 41‐43, 53, 56, 57, 59‐62, 66, 67, 92, 94]. Similar to the works above, these approaches consider a program directly, extract recurrence relations modeling its resource usage and then use sound but incomplete solution methods based on a variety of techniques, such as type systems or separation logic, for general non-polynomial bounds. See [58] for an excellent survey.

In this work, we use a formalism called Generalized Polynomial Recurrence Systems (GPRS), which only employs polynomials in the recurrence relations. We allow recurrence relations such as \(T(n) = 2 \cdot T(n/2) + n^2\) but not \(T(n) = 2 \cdot T(n/2) + 2^n\). In this section, we formally define the concept of a GPRS, its syntax and its semantics.

Recurrence Variables and Valuations. We assume the recurrence relations are defined over a finite set of variables \(\textbf{n}= \{n_1, \ldots , n_k\}\), called recurrence variables. The set of polynomials in the variables \(\textbf{n}\) over the reals is denoted by \(\mathbb {R}[\textbf{n}]\). The domain of our recurrence variables is the set \(\mathbb {R^+}\) of non-negative real numbers. A valuation is a map \(\sigma : \textbf{n}\rightarrow \mathbb {R^+}\). We evaluate a polynomial \(p(\textbf{n})\in \mathbb {R}[\textbf{n}]\) at a valuation \(\sigma \) by substituting each variable n with the value \(\sigma (n)\) and computing p with the usual meaning of multiplication and addition. This evaluation is denoted by either \(\sigma (p(\textbf{n}))\) or \(p(\sigma (\textbf{n}))\).

Recurrence Symbols and Polynomial Calls. A recurrence symbol over \(\textbf{n}\) is simply a function symbol \(T(\textbf{n})\). We denote the set of all recurrence symbols by \(\mathcal {T}\). A polynomial substitution map \(\delta : \textbf{n}\rightarrow \mathbb {R}[\textbf{n}]\) is a function that assigns a polynomial \(p(\textbf{n}) \in \mathbb {R}[\textbf{n}]\) to each variable \(n\in \textbf{n}\). A polynomial substitution map can be applied to a recurrence symbol to get \(\delta (T(\textbf{n})) = T(\delta (\textbf{n}))\). We call \(T(\delta (\textbf{n}))\) the polynomial call of \(T(\textbf{n})\) with respect to \(\delta \). For example, let T(n, m) be a recurrence symbol over \(\textbf{n}= \{n, m\}\) and \(\delta \) a polynomial substitution map with \(\delta (n) = n+m\) and \(\delta (m) = m - 1\). The polynomial call of T(n, m) with respect to \(\delta \) is \(\delta (T(n,m)) = T(\delta (n), \delta (m)) = T(n+m, m-1)\).

Syntax. A Generalized Polynomial Recurrence System (GPRS) is generated from the non-terminal S in the grammar of Figure 1. To make the system more human-readable, we also explicitly write the recurrence variables and symbols at the top of the system as shown in Figure 2.

Monomials and Coefficients. An \(\mathcal {M}\text {-} \texttt {monomial}\) is any expression generated from the non-terminal \(\mathcal {M}\) in the grammar of Figure 1, and an \(\mathcal {R}\text {-} \texttt {expression}\) R is any expression generated from the non-terminal \(\mathcal {R}\). If an \(\mathcal {R}\text {-} \texttt {expression}\) is of the form \(R := f\cdot M + R'\), where M is an \(\mathcal {M}\text {-} \texttt {monomial}\), then f is said to be the coefficient of M. We can evaluate an \(\mathcal {R}\text {-} \texttt {expression}\) R at any valuation \(\sigma \) by applying the substitution \(n \rightarrow \sigma (n)\) in R and simplifying it. We denote this evaluation by \(\sigma (R)\).

GPRS Notation. Based on the discussion above, let \(\mathcal {T}\) be the set of recurrence symbols and \(\textbf{n}\) the set of recurrence variables. A GPRS \(\mathcal {F}(\mathcal {T}, \textbf{n}) = \{\phi _1, \ldots , \phi _m\}\) is a set of blocks with each where each \(R_i\) is an \(\mathcal {R}\text {-} \texttt {expression}\). \(\phi _i.\)

Semantics. Let \(\sigma :\textbf{n}\rightarrow \mathbb {R^+}\) be a valuation. Given a GPRS \(\mathcal {F}\), we interpret each \(\phi \in \mathcal {F}\) as a conditional rewriting rule for \(T(\textbf{n})\). We call \(G(\phi ):= \varphi \) the guard of \(\phi \) and \(\mathcal {R}(\phi ):= (T(\textbf{n}) = R)\) the rewrite rule of \(\phi \). If the valuation \(\sigma \) satisfies the guard \(G(\phi )\), we can invoke the rewrite rule \(\mathcal {R}(\phi )\) of \(\phi \) on \(T(\sigma (\textbf{n}))\) and rewrite \(T(\sigma (\textbf{n})) \rightarrow \sigma (R)\). A rewrite \(R \rightarrow R'\) such that \(R' \ne R\) is called non-trivial.

To be more formal, we define the application of a conditional rewrite rule on an \(\mathcal {R}\text {-} \texttt {expression}\) by structural induction:Evaluations. An evaluation of an \(\mathcal {R}\text {-} \texttt {expression}\) R,  such as \(T(\textbf{n}),\) at a valuation \(\sigma \) in the GPRS \(\mathcal {F}\) is a finite sequence \(\mathcal {E} := R_0 \xrightarrow {\phi _1} R_1 \xrightarrow {\phi _2} \ldots \xrightarrow {\phi _n} R_n\) of non-trivial rewrites such that \(R_0 := \sigma (R),\) \(R_i = \phi _i[R_{i-1}]\) for each \(i \ge 1\), and \(R_n\) is a numerical expression which does not contain any non-terminals and thus can be evaluated to a real number. \(\mathcal {E}(\sigma (R)) := R_n\) is called the value of \(\sigma (R)\) under the evaluation \(\mathcal {E}\). The evaluations are not necessarily unique and we do allow non-determinism. A GPRS \(\mathcal {F}\) is non-deterministic if there are two rules \(\phi , \psi \in \mathcal {F}\) for \(T(\textbf{n})\) and a valuation \(\sigma \) such that \(\sigma \models \phi \) and \(\sigma \models \psi \).

Well-defined GPRS. A GPRS \(\mathcal {F}(\mathcal {T}, \textbf{n})\) is said to be well-defined if for all \(T\in \mathcal {T}\) and valuation \(\sigma : \textbf{n}\rightarrow \mathbb {R^+}\), can be evaluated and every sequence of non-trivial rewrites of \(T(\sigma (\textbf{n}))\) terminates, resulting in a real value.

Positivity. A GPRS \(\mathcal {F}(\mathcal {T},\textbf{n})\) is positive if it has the following two properties:

We now formally define the concept of polynomial bounds.

Polynomial Upper-bound. A polynomial upper-bound of a GPRS \(\mathcal {F}(\mathcal {T}, \textbf{n})\) is a map \(\mathcal {U}: \mathcal {T}\rightarrow \mathbb {R}[\textbf{n}]\) that associates a polynomial \(u_T(\textbf{n})\) to each recurrence symbol \(T \in \mathcal {T}\) such that for every valuation \(\sigma :\textbf{n}\rightarrow \mathbb {R^+}\) and every evaluation \(\mathcal {E}\) of \(T(\sigma (\textbf{n}))\), we have \(u_T(\sigma (\textbf{n})) \ge \mathcal {E}(T(\sigma (\textbf{n})))\). To simplify notation, we would use \(f(\sigma (\textbf{n}))\) and \(f(\sigma )\) interchangeably.

Our goal in this section is to reduce the problem of synthesizing a polynomial upper-bound to solving a system of polynomial constraints in Nonlinear Real Arithmetic (NRA). This corresponds to deciding a formula in the first-order theory of the reals. We first define a polynomial constraint system \(\mathcal {P}\) associated to our GPRS \(\mathcal {F}\). Then, in Theorem 1, we prove that if \(\mathcal {F}\) is well-defined and positive, then any solution of this polynomial constraint system is a valid upper-bound for \(\mathcal {F}\).

Templates. Let \(\mathbb {T}\) be a finite set of variables called template variables. A symbolic polynomial p in \((\textbf{n}, \mathbb {T})\) is a polynomial using the variables in \(\textbf{n}\) in which each coefficient is itself a real polynomial in \(\mathbb {R}[\mathbb {T}]\). Formally, \(p \in \mathbb {R}[\mathbb {T}][\textbf{n}]\). A polynomial template of degree d is a symbolic polynomial p of degree d when seen as a polynomial in \(\textbf{n}.\) A template is canonical if the coefficient of every \(n \in \textbf{n}\) is a distinct template variable \(t_n \in \mathbb T.\) degree 0 or 1 in the variables \(\mathbb {T}\).

Substitution. A symbolic polynomial substitution map \(\mathcal {S}: \mathcal {T}\rightarrow \mathbb {R}[\mathbb {T}][\textbf{n}]\) is a function that maps each recurrence symbol to a polynomial template of degree d. Given an \(\mathcal {R}\text {-} \texttt {expression}\) R, we define \(\mathcal {S}(R)\) as the expression obtained by substituting every T in R with the polynomial \(\mathcal {S}(T)\) and evaluating it.

Polynomial Constraint Systems. Given a symbolic polynomial substitution map \(\mathcal {S}\), the polynomial constraint system \(\mathcal {P}\) of a GPRS \(\mathcal {F}\) with respect to \(\mathcal {S}\) is defined as:

Models. A model or solution of a polynomial constraint system \(\mathcal {P} = \{\phi _1, \ldots , \phi _n\}\) is any valuation \(\varGamma : \mathbb {T} \rightarrow \mathbb {R}\) for the template variables such that \(\varGamma \models \forall \textbf{n}~~ \wedge _{i=1}^{n} \phi _i\).

Suppose the polynomial substitution map \(\mathcal S\) maps every \(T \in \mathcal {T}\) to a canonical template of degree d with fresh template variables. It is easy to verify by definition-chasing that the coefficients in every polynomial upper-bound \(\mathcal U\) of \(\mathcal F\) would then provide a solution for the polynomial constraint system \(\mathcal P.\) For a recurrence variable \(T \in \mathcal {T}\), let us denote the associated polynomial upper bound \(\mathcal {U}(T)\) by \(\mathcal {U}_T.\) We now prove the converse, i.e. that every model of \(\mathcal {P}\) yields a polynomial upper-bound of \(\mathcal {F},\) assuming that our GPRS is both well-defined and positive.

In this section, we describe our sound and semi-complete algorithm for automating the synthesis of polynomial upper bounds for a given GPRS. Our algorithm uses theorems from polyhedral and real algebraic geometry. To improve readability, we first provide the overall algorithm and then fill in the mathematical details in the next section. We assume that the input to our algorithm is a GPRS \(\mathcal F\). Our algorithm consists of the following four steps, which we illustrate by a running example:

Step 1. Initializing a Symbolic Polynomial Substitution Map \(\mathcal {S}\) . The input to our algorithm is a well-defined and positive GPRS \(\mathcal {F}(\mathcal {T}, \textbf{n})\) and a degree bound d. For each recurrence symbol \(T \in \mathcal {T},\) we create a fresh canonical polynomial template \(g_T\) of degree d, where by being fresh we mean that no two polynomial templates share any coefficients in \(\mathbb {T}\). Let \(\mathcal {S}\) be the corresponding symbolic polynomial substitution map.

Step 2. Constructing the Polynomial Constraint System \(\mathcal {P}\) . We compute the polynomial constraint system of \(\mathcal {F}\) with respect to \(\mathcal {S}\) by substituting each recurrence symbol T with its corresponding polynomial \(\mathcal {S}(T)\). Our problem is now reduced to solving a set of constraints of the form

Step 3. Eliminating Quantifier Alternation. This is the main step of our algorithm where we apply various tools from polyhedral and real algebraic geometry to reduce our problem to LP/SDP. The techniques in our arsenal are Putinar’s Positivstellensatz [83], Handelman’s Theorem [51] and the well-known Farkas’ Lemma [46]. Note that to apply Handelman’s Theorem and Putinar’s Postivstellensatz, we have to assume that the set of valuations that satisfy the guard of the constraint forms a compact set². To satisfy this requirement, we can add a constraint of the form \(\sum _{n\in \textbf{n}} n^2 \le N\) to every guard, where \(N \in \mathbb {N}\) is a large number. For example, if all of our parameters are at most \(2^{32},\) we can use \(N = \vert \textbf{n}\vert \cdot 2^{64}.\) This will later come in handy for our completeness result, but our approach is sound even without this modification.

Let \(\exists \mathbb {T} \; \forall \textbf{n}\cdot \varphi \implies g \ge 0\) with \(\varphi = f_1 \ge 0 \wedge \ldots \wedge f_r \ge 0 \) be one of our polynomial constraints with quantifier alternation. Depending upon the degree of the polynomials appearing in this constraint, we apply one of the following cases:

Case 1: \(\varphi \) and g are linear. In this case we use Farkas’ Lemma to reduce this problem to LP. We illustrate this with an example.

Case 2: \(\varphi \) is linear. In this case we use Handelman’s Theorem (Theorem 3). The intuitive idea is to write the RHS not as a linear combination with non-negative coefficients of the LHS itself, but as a combination of products of the inequalities in the LHS.

Case 3: Both \(\varphi \) and g are non-linear. In this case we use Putinar’s Positivstellensatz (Theorem 4).

In this case, we used a simplified template for each \(h_i\). In general, our algorithm creates a template that captures every possible SOS polynomial. This is a standard technique using Cholesky decomposition and leads to an SDP instance instead of LP. See Section 5 for details.

Step 4. Solving the LP/SDP. In the last step, we reduced our problem to solving an LP/SDP instance. Note that Cases 1 and 2, which cover the vast majority of real-world recurrences, are reduced to LP and we need SDP only for Case 3. Moreover, both LP and SDP are solvable in PTIME and there are many scalable tools to handle them. In this step, we pass the LP/SDP to an external solver. At this step, the user can also add an objective function to optimize the bound according to their wishes. For example, one can ask the solver to find the bound that minimizes the coefficient of \(n^2\). We take the solution provided by the solver and plug it back into the template to obtain a polynomial upper-bound for our GPRS. This follows Theorem 1 and concludes our algorithm.

We now provide a formal overview of the theorems from polyhedral and real algebraic geometry used in Section 4.

Sums of Squares. A polynomial \(h(\textbf{n})\) is a sum of squares (SOS) if it can be written as \(h(\textbf{n}) := p_1^2(\textbf{n}) + p_2^2(\textbf{n}) \ldots p_r^2(\textbf{n})\), where each \(p_i \in \mathbb {R}[\textbf{n}]\). We denote the set of all SOS by \(\Sigma _2[\textbf{n}]\).

Closure and Compactness. Given a set \(X \in \mathbb {R}^n\), the closure of X is the set \(\overline{X}\) consisting of X and its boundary. A set X is closed if \(\overline{X} = X\). A set X is bounded if there exists \(c \in \mathbb {R}\) such that \(|x| < c\) for every \(x \in X\). A set is compact if it is both closed and bounded.

Satisfaction Set. Given a conjunction \(\varphi \) of polynomial inequalities of the form \(f(\textbf{n}) \ge 0\) or \(f(\textbf{n}) > 0,\) we define \(\textit{SAT}(\varphi ) := \{\sigma : \textbf{n}\rightarrow \mathbb {R}~\vert ~ \sigma \models \varphi \}\).

Handelman’s Theorem. We define some terminology useful for our next theorem. Let \(F := \{f_1, f_2, \ldots , f_r\}\) be a set of polynomials over \(\mathbb {V}\). We define the monoid of F as the set:In other words, the monoid includes all polynomials that can be obtained as a multiplication of polynomials in F. We also define \(\textit{monoid}_d(F) := \{f \mid f \in \textit{monoid}(F) \wedge \deg (f) \le d\}.\)

As an example, let \( f_1 := (n_1 - 5)\), \(f_2 := (n_2 - 10) \), and \(g := n_1 \cdot n_2 - 5 \cdot n_2 + 1.\) The implication \(\phi := f_1 \ge 0 \wedge f_2 \ge 0 \implies g > 0\) holds for all valuations of \(\{n_1, n_2\}\). We only use the monoid of degree 2 in this example and have \(\textit{monoid}_2(\{f_1, f_2\}) = \{1, f_1, f_2, f_1^2, f_2^2, f_1 \cdot f_2\}. \) It is easy to verify that \(g \equiv 1 + f_1 \cdot f_2 + 10 \cdot f_1\). When relying on Handelman’s theorem, our algorithm sets up a template that includes every polynomial in \(monoid_d(F)\) for a user-defined degree d.

As an example, let \(f_1 := n_1 - 1, f_2 := n_2^2 - 5,\) and \(g := n_1^3 - n_1^2 + n_2^2 + 1.\) The boolean implication \(\varPhi := f_1 \ge 0 \wedge f_2 \ge 0 \implies g > 0\) is valid. We can choose the SOS polynomials \(h_0 = 6, h_1 = n_1^2\) and \(h_2 = 1\), and write \(g \equiv h_0 + h_1 \cdot f_1 + h_2 \cdot f_2\). When relying on Putinar’s Positivstellensatz in our algorithm, we set up a template for each \(h_i\) that can cover all possible SOS of degree d. This is using the following theorems.

To generate a template for an SOS polynomial of degree at most d over the variables \(\textbf{n}\), we first generate a template for the lower-triangular matrix L by creating fresh template variables for each of its non-zero entries. The final template for the SOS polynomial is obtained by setting \( h := V_{d'}^T \cdot L \cdot L^T \cdot V_{d'}. \) This is a standard technique and the reason why applying Putinar’s Positivstellensatz leads to an SDP instance, instead of an LP instance as in the cases of Farkas and Handelman. See [49, Section 2.7] for examples and [6] for extensions to other combinations of strict/non-strict inequalities. Based on the theorems above, we have the following soundness and semi-completeness result:

Although our approach is designed for polynomial recurrences and upper-bounds, it is also extensible using standard variable substitution techniques and can thus synthesize exponential bounds or generalized polynomial bounds with rational (non-integral) degrees.

Generalized Polynomials. Let \(\textbf{n}= \{n_1, \ldots , n_k\}\) be a set of non-negative recurrence variables and \(q \in \mathbb {N}^+\) a positive integer. We define new variablesA generalized q-polynomial over \(\textbf{n}\) is simply a polynomial over \(\{m_1, \ldots , m_k\}\). We show the set of generalized q-polynomials over \(\textbf{n}\) by \(\mathbb {R}_q[\textbf{n}] := \mathbb {R}[n_1^{1/q}, \ldots , n_k^{1/q}].\) For a generalized q-polynomial p over \(\textbf{n},\) we define the degree of p as its degree over the \(m_i\)’s divided by q.

Extending Our Approach to Generalized Polynomials. To find generalized polynomial upper-bounds, it suffices to write our original GPRS in terms of the new variables, solve it using the algorithm of Section 4, and then rewrite the solution using the original variables.

Exponential Bounds. Applying the standard technique of \(\log \)-substitution, our approach is able to obtain exponential upper-bounds as well.

Our main theoretical contribution in this work is the completeness of our algorithm. Such completeness results usually come at the cost of sacrificing practicality. For example, decision procedures for the existential theory of the reals are notoriously unscalable and not applicable to any real-world or even toy use-case. In contrast, our algorithm reduces the problem to LP/SDP, for which there are plenty of efficient solvers. Thus, we now provide experimental results demonstrating that, in addition to its completeness, our approach is practical and efficiently solves a variety of recurrence systems taken from three categories in the literature. We implemented our algorithm in C++ and used the Mosek Optimization Suite [79] to solve LP/SDP instances. Our tool is free and open-source and can be accessed at [81] (https://​doi.​org/​10.​5281/​zenodo.​14836308). All results were obtained on an AMD Ryzen 5 4600H Machine (3 GHz, 12 cores) running Ubuntu 20.04 LTS with 16 GB of RAM.

A. Invariant Generation in Probabilistic Programs. Our first category of benchmark GPRSs come from invariant generation. The works [10, 78] provide an algorithm and tool, called Polar, to generate moment-based invariants for a wide family of loops in probabilistic programs, called prob-solvable loops. The algorithm first extracts a recurrence system which connects the moments of program variables and then attempts to solve it.

As the simplest example, consider the program above, where uniform(0, 1) denotes a sample taken from the uniform distribution on [0, 1]. This loop computes part of the summation \(\textstyle \sum _{y = 1}^\infty y\) where each term is taken with probability 1/2. Let Ex(n) and Ey(n) denote the expected values of the variables after n iterations. The work [10] obtains the following recurrence system:

Our approach can be directly applied to this GPRS and provides the following solution: \(\mathbb {E}x(n) = 0.25 \cdot n^{2} + 0.25 \cdot n,\) and \(\mathbb {E}y(n) = n.\)

Table 1 provides a list of probabilistic programs from [10] that can be encoded in our GPRS framework. Our approach could successfully and efficiently solve these recurrence systems and compute the moments. Table 1 shows that (i) our approach is able to handle systems of recurrences which are beyond the scope of MT and AB, and (ii) in addition to completeness, we preserve practicality and solve each recurrence system within a few seconds, with most cases taking less than a second. In comparison, Polar is efficient but lacks completeness. Conversely, it can handle non-polynomial recurrences which are not supported in our GPRS framework.

B. Resource Usage of Functional Programs. RaML [54, 55] is a framework based on type theory to analyze and bound the resource consumption of functional programs written in OCaml. The resource in question can be time or space or arbitrarily defined by assigning costs to certain operations in the program. This was later extended in PUBS [4, 5]. As before, these approaches first find a system of recurrences and then solve it to find a bound, e.g. this GPRS models a program performing the sieve of Eratosthenes [55]:

This example cannot be handled by either MT or AB, since it has two functions referring to each other and a function with two variables. Our approach obtains the bounds \(\texttt {eratos}(n) \le 0.5 \cdot n^{2} + 1.5 \cdot n + 1\) and \(\texttt {filter}(x, m) \le m + 1.\)

Table 2 provides a list of functional programs from [54, 55] whose resource usage can be modeled by a polynomial recurrence system. It also reports the resource usage bounds obtained by our approach and the previous tools, especially CHORA [15], which is the closest related work. Table 2 shows that (i) our approach is practical and successfully handles non-trivial systems of recurrences, (ii) the bounds obtained by our approach on these programs are either tighter than the previous methods, the same, or incomparable. Recall that our approach is able to find the best polynomial bound w.r.t. any user-defined objective function. Thus, it is able to synthesize the same polynomial bounds as previous tools, too. In Table 2, we are not reporting the runtimes since the results were obtained using previous methods’ web interfaces and not on our machine. PUBS is proprietary and no source code or executable is available for it. Thus, we do not claim to be faster than them, but rather to be the first approach for polynomial recurrences with both practicality and completeness guarantees.

C. Classical Algorithms. We consider four classical algorithms for which the best known runtime bound is not polynomial. This includes Strassen’s matrix multiplication algorithm, Karatsuba’s multiplication, fast exponentiation by squaring, and merge sort. We used the following recurrences:

Table 3 shows our experimental results in comparison with CHORA [15]. Although our approach cannot find the optimal answer since it is not polynomial, using the trick of Section 6 works well in practice and obtains close-to-optimal results. We generally observe that CHORA is faster. This is due to the high degree of polynomials needed in templates to model non-integer degrees. Conversely, our completeness pays off in practice and our approach is able to find a tighter bound for fast exponentiation.

D. Ablation Study. Finally, we performed an ablation study to measure the practical impact of Step 3 of our algorithm, i.e. the application of Farkas, Handelman and Putinar theorems. To this end, we passed the constraints generated by the end of Step 2, which are formulas in the first-order theory of the reals with an \(\exists \forall \) quantifier alternation, directly to state-of-the-art SMT solvers, including Z3 [80], cvc4 [9], cvc5 [8] and Vampire [73]. The latter two are the winners of the non-linear real arithmetic competition track of SVCOMP [13]. With a time limit of 12 hours per solver per instance, none of the solvers were able to handle our benchmarks. Thus, the dedicated quantifier elimination methods are necessary not only theoretically but also in practice.

In summary, in addition to providing completeness guarantees for systems of polynomial recurrences, our approach remains practical. To our knowledge, polynomial recurrence systems are one of the most expressive families of recurrences to date to be solved by a complete method and are not subsumed by any of the previous approaches. We also showed that our approach successfully synthesizes bounds for benchmarks that were beyond the scope of previous complete methods, i.e. MT and AB (Tables 1 and 2) and that it can find close-to-optimal bounds even in cases where the optimal solution is not a polynomial (Table 3). Additionally, due to its completeness, it often finds tighter bounds than previous methods and can handle instances that were not solvable by CHORA.

In this work, we considered Generalized Polynomial Recurrence Systems (GPRS), a wide family of recurrences that allows (i) a system of interdependent recurrence relations, (ii) an arbitrary number of variables, and (iii) conditional recurrence rules. We provided an automated template-based algorithm for finding polynomial solutions, i.e. upper-bounds, for such recurrences. Our algorithm is sound and semi-complete and guaranteed to find the tightest possible polynomial bounds with respect to any user-defined objective function. Moreover, for any fixed degree of polynomial templates, its complexity is PTIME.