Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds
Krishnendu Chatterjee, Hongfei Fu, Aniket Murhekar

TL;DR
This paper introduces a fast, sound algorithm for automatically deriving almost-linear expected-runtime bounds for recurrence relations in randomized algorithms, improving analysis efficiency over traditional methods.
Contribution
The paper presents a simple linear-time algorithm that automatically infers optimal expected-runtime bounds for classical randomized algorithms, enhancing analysis efficiency and accuracy.
Findings
Efficiently derives expected-runtime bounds for classical randomized algorithms.
Successfully infers asymptotically optimal bounds for algorithms like QUICK-SORT and COUPON-COLLECTOR.
Implemented approach demonstrates practical efficiency in experimental evaluations.
Abstract
We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. Several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., QUICK-SORT), or completely ineffective (e.g., COUPON-COLLECTOR). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear, or almost-linear (, , , respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. Our approach can infer the asymptotically optimal…
| Notation | Expression | , -term | Over-approximation |
| , | |||
| , | |||
| , | |||
| , | |||
| , | |||
| , -term | Over-approximation | , -term | Over-approximation |
| , | , | ||
| , | , | ||
| , | , | ||
| , | , | ||
| , | , | ||
| Recur. Rel. | Recur. Rel. | ||||||||
| R.-Sear. | UniDec | ✓ | Sort-Sel. | UniDec | ✓ | ||||
| Q.-Sort | UniDec | ✓ | Coupon | UniDec | ✓ | ||||
| Q.-Select | UniDec | ✓ | Res. A | UniDec | ✓ | ||||
| Diam. A | UniDec | ✓ | Res. B | UniDec | ✓ | ||||
| Diam. B | UniDec | ✓ | - | - | - | - | - | ||
| - | - | ||||||||
| - | - | ||||||||
| - | - | ||||||||
| - | - |
| Program | UniDec | UniSynth(✓) | ||||
| R.-Sear. | ✓ | |||||
| Q.-Sort | - | - | - | - | ||
| ✓ | ||||||
| Q.-Select | - | - | - | - | ||
| ✓ | ||||||
| Diam. A | - | - | - | - | ||
| ✓ | ||||||
| Diam. B | - | - | - | - | ||
| ✓ | ||||||
| Sort-Sel. | - | - | - | - | ||
| ✓ | ||||||
| Coupon | ✓ | |||||
| Res. A | ✓ | |||||
| Res. B | - | - | - | - | ||
| ✓ | ||||||
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
11institutetext: IST Austria, Klosterneuburg, Austria 22institutetext: State Key Laboratory of Computer Science, Institute of Software
Chinese Academy of Sciences, Beijing, P.R. China 33institutetext: IIT Bombay, India
Automated Recurrence Analysis
for Almost-Linear Expected-Runtime Bounds
Krishnendu Chatterjee 11
Hongfei Fu 22
Aniket Murhekar 33
Abstract
We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. Several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear, or almost-linear (, , , respectively, where represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. Our approach can infer the asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select, Coupon-Collector, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic of expected-runtime, or quadratic as compared to linear or almost-linear of expected-runtime), or ineffective. We have implemented our approach, and the experimental results show that we obtain the bounds efficiently for the recurrences of various classical algorithms.
1 Introduction
Static analysis for quantitative bounds. Static analysis of programs aims to reason about programs without running them. The most basic properties for static analysis are qualitative properties, such as safety, termination, liveness, that for every trace of a program gives a Yes or No answer (such as assertion violation or not, termination or not). However, recent interest in analysis of resource-constrained systems, such as embedded systems, as well as for performance analysis, quantitative performance characteristics are necessary. For example, the qualitative problem of termination asks whether a given program always terminates, whereas the quantitative problem asks to obtain precise bounds on the number of steps, and is thus a more challenging problem. Hence the problem of automatically reasoning about resource bounds (such as time complexity bounds) of programs is both of significant theoretical as well as practical interest.
Worst-case bounds. The worst-case analysis of programs is the fundamental problem in computer science, which is the basis of algorithms and complexity theory. However, manual proofs of worst-case analysis can be tedious and also require non-trivial mathematical ingenuity, e.g., the book The Art of Computer Programming by Knuth presents a wide range of involved techniques to derive such precise bounds [37, 38]. There has been a considerable research effort for automated analysis of such worst-case bounds for programs, see [23, 24, 26, 27] for excellent expositions on the significance of deriving precise worst-case bounds and the automated methods to derive them. For the worst-case analysis there are several techniques, such as worst-case execution time analysis [47], resource analysis using abstract interpretation and type systems [24, 2, 34, 26, 27], ranking functions [8, 9, 15, 42, 45, 17, 48, 43], as well as recurrence relations [21, 2, 3, 4].
Expected-runtime bounds. While several works have focused on deriving worst-case bounds for programs, quite surprisingly little work has been done to derive precise bounds for expected-runtime analysis, with the exception of [20], which focuses on randomization in combinatorial structures (such as trees). This is despite the fact that expected-runtime analysis is an equally important pillar of theoretical computer science, both in terms of theoretical and practical significance. For example, while for real-time systems with hard constraints worst-case analysis is necessary, for real-time systems with soft constraints the more relevant information is the expected-runtime analysis. Below we highlight three key significance of expected-runtime analysis.
Simplicity and desired properties: The first key aspect is simplicity: often much simpler algorithms (thus simple and efficient implementations) exist for expected-runtime complexity as compared to worst-case complexity. A classic example is the Selection problem that given a set of numbers and , asks to find the -th largest number (eg, for median ). The classical linear-time algorithm for the problem (see [16, Chapter 9]) is quite involved, and its worst-case analysis to obtain linear time bound is rather complex. In contrast, a much simpler algorithm exists (namely, Quick-Select) that has linear expected-runtime complexity. Moreover, randomized algorithms with expected-runtime complexity enjoy many desired properties, which deterministic algorithms do not have. A basic example is Channel-Conflict Resolution (see Example 7, Section 2.4) where the simple randomized algorithm can be implemented in a distributed or concurrent setting, whereas deterministic algorithms are quite cumbersome. 2. 2.
Efficiency in practice: Since worst-case analysis concerns with corner cases that rarely arise, many algorithms and implementations have much better expected-runtime complexity, and they perform extremely well in practice. A classic example is the Quick-Sort algorithm, that has quadratic worst-case complexity, but almost linear expected-runtime complexity, and is one of the most efficient sorting algorithms in practice. 3. 3.
Worst-case analysis ineffective: In several important cases the worst-case analysis is completely ineffective. For example, consider one of the textbook stochastic process, namely the Coupon-Collector problem, where there are types of coupons to be collected, and in each round, a coupon type among the types is obtained uniformly at random. The process stops when all types are collected. The Coupon-Collector process is one of the basic and classical stochastic processes, with numerous applications in network routing, load balancing, etc (see [40, Chapter 3] for applications of Coupon-Collector problems). For the worst-case analysis, the process might not terminate (worst-case bound infinite), but the expected-runtime analysis shows that the expected termination time is .
Challenges. The expected-runtime analysis brings several new challenges as compared to the worst-case analysis. First, for the worst-case complexity bounds, the most classical characterization for analysis of recurrences is the Master Theorem (cf. [16, Chapter 1]) and Akra-Bazzi’s Theorem [1]. However, the expected-runtime analysis problems give rise to recurrences that are not characterized by these theorems since our recurrences normally involve an unbounded summation resulting from a randomized selection of integers from to where is unbounded. Second, techniques like ranking functions (linear or polynomial ranking functions) cannot derive efficient bounds such as or . While expected-runtime analysis has been considered for combinatorial structures using generating function [20], we are not aware of any automated technique to handle recurrences arising from randomized algorithms.
Analysis problem. We consider the algorithmic analysis problem of recurrences arising naturally for randomized recursive programs. Specifically we consider the following:
- •
We consider two classes of recurrences: (a) univariate class with one variable (which represents the array length, or the number of input elements, as required in problems such as Quick-Select, Quick-Sort etc); and (b) separable bivariate class with two variables (where the two independent variables represent the total number of elements and total number of successful cases, respectively, as required in problems such as Coupon-Collector, Channel-Conflict Resolution). The above two classes capture a large class of expected-runtime analysis problems, including all the classical ones mentioned above. Moreover, the main purpose of expected-runtime analysis is to obtain efficient bounds. Hence we focus on the case of logarithmic, linear, and almost-linear bounds (i.e., bounds of form , and , respectively, where is the size of the input). Moreover, for randomized algorithms, quadratic bounds or higher are rare.
Thus the main problem we consider is to automatically derive such efficient bounds for randomized univariate and separable bivariate recurrence relations.
Our contributions. Our main contribution is a sound approach for analysis of recurrences for expected-runtime analysis. The input to our problem is a recurrence relation and the output is either logarithmic, linear, or almost-linear as the asymptotic bound, or fail. The details of our contributions are as follows:
Efficient algorithm. We first present a linear-time algorithm for the univariate case, which is based on simple comparison of leading terms of pseudo-polynomials. Second, we present a simple reduction for separable bivariate recurrence analysis to the univariate case. Our efficient (linear-time) algorithm can soundly infer logarithmic, linear, and almost-linear bounds for recurrences of one or two variables. 2. 2.
Analysis of classical algorithms. We show that for several classical algorithms, such as Randomized-Search, Quick-Select, Quick-Sort, Coupon-Collector, Channel-Conflict Resolution (see Section 2.2 and Section 2.4 for examples), our sound approach can obtain the asymptotically optimal expected-runtime bounds for the recurrences. In all the cases above, either the worst-case bounds (i) do not exist (e.g., Coupon-Collector), or (ii) are quadratic when the expected-runtime bounds are linear or almost-linear (e.g., Quick-Select, Quick-Sort); or (iii) are linear when the expected-runtime bounds are logarithmic (e.g., Randomized-Search). Thus in cases where the worst-case bounds are either not applicable, or grossly overestimate the expected-runtime bounds, our technique is both efficient (linear-time) and can infer the optimal bounds. 3. 3.
Implementation. Finally, we have implemented our approach, and we present experimental results on the classical examples to show that we can efficiently achieve the automated expected-runtime analysis of randomized recurrence relations.
Novelty and technical contribution. The key novelty of our approach is an automated method to analyze recurrences arising from randomized recursive programs, which are not covered by Master theorem. Our approach is based on a guess-and-check technique. We show that by over-approximating terms in a recurrence relation through integral and Taylor’s expansion, we can soundly infer logarithmic, linear and almost-linear bounds using simple comparison between leading terms of pseudo-polynomials.
2 Recurrence Relations
We present our mini specification language for recurrence relations for expected-runtime analysis. The language is designed to capture running time of recursive randomized algorithms which involve (i) only one function call whose expected-runtime complexity is to be determined, (ii) at most two integer parameters, and (iii) involve randomized-selection or divide-and-conquer techniques. We present our language separately for the univariate and bivariate cases. In the sequel, we denote by , , , and the sets of all positive integers, non-negative integers, integers, and real numbers, respectively.
2.1 Univariate Randomized Recurrences
Below we define the notion of univariate randomized recurrence relations. First, we introduce the notion of univariate recurrence expressions. Since we only consider single recursive function call, we use ‘’ to represent the (only) function call. We also use ‘’ to represent the only parameter in the function declaration.
Univariate recurrence expressions. The syntax of univariate recurrence expressions is generated by the following grammar:
[TABLE]
where and represents the natural logarithm function with base . Informally, is the (expected) running time of a recursive randomized program which involves only one recursive routine indicated by and only one parameter indicated by . Then each -term in the grammar has a direct algorithmic meaning:
- •
may mean a recursion to a sub-array with length decremented by one;
- •
and may mean a recursion related to a divide-and-conquer technique;
- •
finally, may mean a recursion related to a randomized selection of an array index.
Substitution. Consider a function and univariate recurrence expression . The substitution function, denoted by , is the function from into such that the value for is obtained by evaluation through substituting for and for in , respectively. Moreover, if does not involve the appearance of ‘’, then we use the abbreviation i.e., omit . For example, (i) if , and , then is the function , and (ii) if , then is .
Univariate recurrence relation. A univariate recurrence relation is a pair of equalities as follows:
[TABLE]
where and is a univariate recurrence expression. For a univariate recurrence relation the evaluation sequence is as follows: , and for , given for , for the value we evaluate the expression , since in the parameter always decreases and is thus well-defined.
Finite vs infinite solution. Note that the above description gives a computational procedure to compute for any finite , in linear time in through dynamic programming. The interesting question is to algorithmically analyze the infinite behavior. A function is called a solution to if for all . The function is unique and explicitly defined as follows: (1) Base Step. ; and (2) Recursive Step. for all . The interesting algorithmic question is to reason about the asymptotic infinite behaviour of .
2.2 Motivating Classical Examples
In this section we present several classical examples of randomized programs whose recurrence relations belong to the class of univariate recurrence relations described in Section 2.1. We put details of pseudocode and how to derive the recurrence relations in this section in Appendix 0.A. Moreover in all cases the base step is , hence we discuss the recursive case.
Example 1* (*Randomized-Search)
Consider the Sherwood’s Randomized-Search algorithm (cf. [39, Chapter 9]). The algorithm checks whether an integer value is present within the index range () in an integer array which is sorted in increasing order and is without duplicate entries. The algorithm outputs either the index for in or meaning that is not present in the index range of . The recurrence relation for this example is as follows:
[TABLE]
We note that the worst-case complexity for this algorithm is .∎
Example 2* (*Quick-Sort)
Consider the Quick-Sort algorithm [16, Chapter 7]. The recurrence relation for this example is:
[TABLE]
where represents the maximal expected execution time where is the array length and the execution time of pivoting is represented by . We note that the worst-case complexity for this algorithm is .∎
Example 3* (*Quick-Select)
Consider the Quick-Select algorithm (cf. [16, Chapter 9]). The recurrence relation for this example is
[TABLE]
We note that the worst-case complexity for this algorithm is .∎
Example 4* (*Diameter-Computation)
Consider the Diameter-Computation algorithm (cf. [40, Chapter 9]) to compute the diameter of an input finite set of three-dimensional points. Depending on Eucledian or metric we obtain two different recurrence relations. For Eucledian we have the following relation:
[TABLE]
and for metric we have the following relation:
[TABLE]
We note that the worst-case complexity for this algorithm is as follows: for Euclidean metric it is and for the metric it is .∎
Example 5 (Sorting with Quick-Select)
Consider a sorting algorithm which selects the median through the Quick-Select algorithm. The recurrence relation is directly obtained as follows:
[TABLE]
where is an upper bound on the expected running time of Quick-Select (cf. Example 3). We note that the worst-case complexity for this algorithm is .∎
2.3 Separable Bivariate Randomized Recurrences
We consider a generalization of the univariate recurrence relations to a class of bivariate recurrence relations called separable bivariate recurrence relations. Similar to the univariate situation, we use ‘’ to represent the (only) function call and ‘’, ‘’ to represent namely the two integer parameters.
Separable Bivariate Recurrence Expressions. The syntax of separable bivariate recurrence expressions is illustrated by and as follows:
[TABLE]
The differences are that (i) we have two independent parameters , (ii) now represents an expression composed of only -terms, and (iii) (resp. ) represents arithmetic expressions for (resp. for ). This class of separable bivariate recurrence expressions (often for brevity bivariate recurrence expressions) stresses a dominant role on and a minor role on , and is intended to model randomized algorithms where some parameter (to be represented by ) does not change value.
Substitution. The notion of substitution is similar to the univariate case. Consider a function , and a bivariate recurrence expression . The substitution function, denoted by , is the function from into such that is the real number evaluated through substituting for , respectively. The substitution for is defined in a similar way, with the difference that they both induce a univariate function.
Bivariate recurrence relations. We consider bivariate recurrence relations , which consists of two equalities of the following form:
[TABLE]
where and are from the grammar above.
Solution to bivariate recurrence relations. The evaluation of bivariate recurrence relation is similar to the univariate case. Similar to the univariate case, the unique solution to a recurrence relation taking the form (8) is a function defined recursively as follows: (1) Base Step. for all ; and (2) Recursive Step. for all and . Again the interesting algorithmic question is to reason about the infinite behaviour of .
2.4 Motivating Classical Examples
In this section we present two classical examples of randomized algorithms where the randomized recurrence relations are bivariate. We put the detailed illustration for this two examples in Appendix 0.B.
Example 6* (*Coupon-Collector)
Consider the Coupon-Collector problem [40, Chapter 3] with different types of coupons (). The randomized process proceeds in rounds: at each round, a coupon is collected uniformly at random from the coupon types the rounds continue until all the types of coupons are collected. We model the rounds as a recurrence relation with two variables , where represents the total number of coupon types and represents the remaining number of uncollected coupon types. The recurrence relation is as follows:
[TABLE]
where is the expected number of rounds. We note that the worst-case complexity for this process is .∎
Example 7* (*Channel-Conflict Resolution)
We consider two network scenarios in which clients are trying to get access to a network channel. This problem is also called the Resource-Contention Resolution [36, Chapter 13]. In this problem, if more than one client tries to access the channel, then no client can access it, and if exactly one client requests access to the channel, then the request is granted. In the distributed setting, the clients do not share any information. In this scenario, in each round, every client requests an access to the channel with probability . Then for this scenario, we obtain an over-approximating recurrence relation
[TABLE]
for the expected rounds until which every client gets at least one access to the channel. In the concurrent setting, the clients share one variable, which is the number of clients which has not yet been granted access. Also in this scenario, once a client gets an access the client does not request for access again. For this scenario, we obtain an over-approximating recurrence relation
[TABLE]
We also note that the worst-case complexity for both the scenarios is .∎
3 Expected-Runtime Analysis
We focus on synthesizing logarithmic, linear, and almost-linear asymptotic bounds for recurrence relations. Our goal is to decide and synthesize asymptotic bounds in the simple form: . Informally, is the major term for time complexity, is the coefficient of to be synthesized, and is the time complexity for the base case specified in (1) or (8).
Univariate Case: The algorithmic problem in univariate case is as follows:
- •
Input: a univariate recurrence relation taking the form (1) and an expression .
- •
Output: Decision problem. Output “yes” if , and “fail” otherwise.
- •
Output: Quantitative problem. A positive real number such that
[TABLE]
for all , or “fail” otherwise, where is from (1).
Remark 1
First note that while in the problem description we consider the form part of input for simplicity, since there are only three possibilites we can simply enumerate them, and thus have only the recurrence relation as input. Second, in the algorithmic problem above, w.l.o.g, we consider that every in (1) or (8) involves at least one -term and one non--term; this is natural since (i) for algorithms with recursion at least one -term should be present for the recursive call and at least one non--term for non-recursive base step. ∎
Bivariate Case: The bivariate-case problem is an extension of the univariate one, and hence the problem definitions are similar, and we present them succinctly below.
- •
Input: a bivariate recurrence relation taking the form (8) and an expression (similar to the univariate case).
- •
Output: Decision problem. Output “yes” if , and “fail” otherwise;
- •
Output: Quantitative problem. A positive real number such that for all , or “fail” otherwise, where are from (8). Note that in the expression above the term does not appear as it can be captured with itself.
Recall that in the above algorithmic problems obtaining the finite behaviour of the recurrence relations is easy (through evaluation of the recurrences using dynamic programming), and the interesting aspect is to decide the asymptotic infinite behaviour.
4 The Synthesis Algorithm
In this section, we present our algorithms to synthesize asymptotic bounds for randomized recurrence relations.
Main ideas. The main idea is as follows. Consider as input a recurrence relation taking the form (1) and an univariate recurrence expression which specifies the desired asymptotic bound. We first define the standard notion of a guess-and-check function which provides a sound approach for asymptotic bound. Based on the guess-and-check function, our algorithm executes the following steps for the univariate case.
First, the algorithm sets up a scalar variable and then constructs the template to be for a univariate guess-and-check function. 2. 2.
Second, the algorithm computes an over-approximation of such that the over-approximation will involve terms from (for ) only. Note that may be greater than , so the above expressions are not necessarily linear (they can be quadratic or cubic for example). 3. 3.
Finally, the algorithm synthesizes a value for such that for all through truncation of into a finite range and a limit behaviour analysis (towards ).
Our algorithm for bivariate cases is a reduction to the univariate case.
Guess-and-Check functions. We follow the standard guess-and-check technique to solve simple recurrence relations. Below we first fix a univariate recurrence relation taking the form (1). By an easy induction on (starting from the specified in Definition 1) we obtain Theorem 4.1.
Definition 1 (Univariate Guess-and-Check Functions)
Let be a univariate recurrence relation taking the form (1). A function is a guess-and-check function for if there exists a natural number such that: (1) (Base Condition) for all , and (2) (Inductive Argument) for all .
Theorem 4.1 (Guess-and-Check, Univariate Case)
If a function is a guess-and-check function for a univariate recurrence relation taking the form (1), then for all .
We do not explicitly present the definition for guess-and-check functions in the bivariate case, since we will present a reduction of the analysis of separable bivariate recurrence relations to that of the univariate ones (cf. Section 4.2).
Overapproximations for Recurrence Expressions. We now develop tight overapproximations for logarithmic terms. In principle, we use Taylor’s Theorem to approximate logarithmic terms such as , and integral to approximate summations of logarithmic terms. All the results below are technical and depends on basic calculus (the detailed proofs are in the Appendix 0.C).
Proposition 1
For all natural number :
[TABLE]
Proposition 2
For all natural number : .
Proposition 3
For all natural number :
- •
;
- •
;
- •
.
Note that Proposition 3 is non-trivial since it approximates summation of reciprocal and logarithmic terms up to a constant deviation. For example, one may approximate directly by , but this approximation deviates up to a logarithmic term from Proposition 3. From Proposition 3, we establish a tight approximation for summation of logarithmic or reciprocal terms.
Example 8
Consider the summation . By Proposition 3, we can over-approximate it as
[TABLE]
where . By using Proposition 1, the above expression is roughly (for details see Appendix 0.C).∎
Remark 2
Although we do approximation for terms related to only almost-linear bounds, Proposition 3 can be extended to logarithmic bounds with higher degree (e.g., ) since integration of such bounds can be obtained in closed forms.∎
4.1 Algorithm for Univariate Recurrence Relations
We present our algorithm to synthesize a guess-and-check function in form (12) for univariate recurrence relations. We present our algorithm in two steps. First, we present the decision version, and then we present the quantitative version that synthesizes the associated constant. The two key aspects are over-approximation and use of pseudo-polynomials, and we start with over-approximation. We relegate some technical details to Appendix 0.D.
Definition 2 (Overapproximation)
Let . Consider a univariate recurrence expression , constants and , and the function . We define the over-approximation function, denoted , recursively as follows.
- •
Base Step A. If is one of the following: , then .
- •
Base Step B. If is a single term which involves , then we define from over-approximations Proposition 1– 3. In details, is obtained from by first over-approximating any summation through Proposition 3 (i.e., through those functions defined below Proposition 3), then over-approximating any by Proposition 1 and Proposition 2. The details of the important over-approximations are illustrated explicitly in Table 1.
- •
Recursive Step. We have two cases: (a) If is , then is . (b) If is , then is .
Example 9
Consider the recurrence relation for Sherwood’s Randomized-Search (cf. (2)). Choose and then the template becomes . From Example 8, we have that the over-approximation for when is (the second summand comes from an over-approximation of ).∎
Remark 3
Since integrations of the form can be calculated in closed forms (cf. Remark 2), Table 1 can be extended to logarithmic expressions with higher order, e.g., .∎
Pseudo-polynomials. Our next step is to define the notion of (univariate) pseudo-polynomials which extends normal polynomials with logarithm. This notion is crucial to handle inductive arguments in the definition of (univariate) guess-and-check functions.
Definition 3 (Univariate Pseudo-polynomials)
A univariate pseudo-polynomial (w.r.t logarithm) is a function such that there exist non-negative integers and real numbers ’s such that for all ,
[TABLE]
W.l.o.g, we consider that in the form (13), it holds that (i) , (ii) either or , and (iii) similarly either or .
Degree of pseudo-polynomials. Given a univariate pseudo-polynomial in the form (13), we define the degree of by: if and otherwise. Intuitively, if the term with highest degree involves logarithm, then we increase the degree by , else it is the power of the highest degree term.
Leading term . The leading term of a pseudo-polynomial in the form (13) is a function defined as follows: ; and ; for all . Furthermore, we define to be the (only) coefficient of .
With the notion of pseudo-polynomials, the inductive argument of guess-and-check functions can be soundly transformed into an inequality between pseudo-polynomials.
Lemma 1
Let and be a constant. For all univariate recurrence expressions , there exists pseudo-polynomials and such that coefficients (i.e., ’s in (13)) of are all non-negative, and the following assertion holds: for all and for all , with , the inequality is equivalent to .
Remark 4
In the above lemma, though we only refer to existence of pseudo-polynomials and , they can actually be computed in linear time, because and are obtained by simple rearrangements of terms from and , respectively.
Example 10
Let us continue with Sherwood’s Randomized-Search. Again choose . From Example 9, we obtain that for every , the inequality
[TABLE]
resulting from over-approximation and the inductive argument of guess-and-check functions is equivalent to .∎
As is indicated in Definition 1, our aim is to check whether holds for sufficiently large . The following proposition provides a sufficient and necessary condition for checking whether holds for sufficiently large .
Proposition 4
Let be pseudo-polynomials such that and all coefficients of are non-negative. Then there exists a real number such that for sufficiently large iff and .
Note that by Definition 1 and the special form (12) for univariate guess-and-check functions, a function in form (12) needs only to satisfy the inductive argument in order to be a univariate guess-and-check function: once a value for is synthesized for a sufficiently large , one can scale the value so that the base condition is also satisfied. Thus from the sufficiency of Proposition 4, our decision algorithm that checks the existence of some guess-and-check function in form (12) is presented below. Below we fix an input univariate recurrence relation taking the form (1) and an input expression .
Algorithm UniDec: Our algorithm, namely UniDec, for the decision problem of the univariate case, has the following steps.
Template. The algorithm establishes a scalar variable and sets up the template for a univariate guess-and-check function. 2. 2.
Over-approximation. Let denote . The algorithm calculates the over-approximation function , where is from (1). 3. 3.
Transformation. The algorithm transforms the inequality for inductive argument of guess-and-check functions through Lemma 1 equivalently into , where are pseudo-polynomials obtained in linear-time through rearrangement of terms from and (see Remark 4). 4. 4.
Coefficient Checking. The algorithm examines cases on . If and , then algorithm outputs “yes” meaning that “there exists a univariate guess-and-check function”; otherwise, the algorithm outputs “fail”.
Theorem 4.2 (Soundness for UniDec)
If UniDec outputs “yes”, then there exists a univariate guess-and-check function in form (12) for the inputs and . The algorithm is a linear-time algorithm in the size of the input recurrence relation.
Example 11
Consider Sherwood’s Randomized-Search recurrence relation (cf. (2)) and as the input. As illustrated in Example 9 and Example 10, the algorithm asserts that the asymptotic behaviour is .∎
Remark 5
From the tightness of our over-approximation (up to only constant deviation) and the sufficiency and necessity of Proposition 4, the UniDec algorithm can handle a large class of univariate recurrence relations. Moreover, the algorithm is quite simple and efficient (linear-time). However, we do not know whether our approach is complete. We suspect that there is certain intricate recurrence relations that will make our approach fail.
Analysis of examples of Section 2.2. Our algorithm can decide the following optimal bounds for the examples of Section 2.2.
For Example 1 we obtain an bound (recall worst-case bound is ). 2. 2.
For Example 2 we obtain an bound (recall worst-case bound is ). 3. 3.
For Example 3 we obtain an bound (recall worst-case bound is ). 4. 4.
For Example 4 we obtain an (resp. ) bound for Euclidean metric (resp. for metric), whereas the worst-case bound is (resp. ). 5. 5.
For Example 5 we obtain an bound (recall worst-case bound is ).
In all cases above, our algorithm decides the asymptotically optimal bounds for the expected-runtime analysis, whereas the worst-case analysis grossly over-estimate the expected-runtime bounds.
Quantitative bounds. Above we have already established that our linear-time decision algorithm can establish the asymptotically optimal bounds for the recurrence relations of several classical algorithms. We now take the next step to obtain even explicit quantitative bounds, i.e., to synthesize the associated constants with the asymptotic complexity. To tackle these situations, we derive a following proposition which gives explicitly a threshold for “sufficiently large numbers”. We first explicitly constructs a threshold for “sufficiently large numbers”. Then we show in Proposition 5 that is indeed what we need.
Definition 4 (Threshold for Sufficiently Large Numbers)
Let be two univariate pseudo-polynomials , such that and . Then given any , the number is defined as the smallest natural number such that both (defined below) is smaller than :
- •
;
- •
.
where equals when and [math] otherwise.
Proposition 5
Consider two univariate pseudo-polynomials such that , all coefficients of are non-negative and . Then given any , for all (for of Definition 4).
With Proposition 5, we describe our algorithm UniSynth which outputs explicitly a value for (in (12)) if UniDec outputs yes. Below we fix an input univariate recurrence relation taking the form (1) and an input expression . Moreover, the algorithm takes as another input, which is basically a parameter to choose the threshold for finite behaviour. For example, smaller leads to large threshold, and vice-versa. Thus we provide a flexible algorithm as the threshold can be varied with the choice of .
Algorithm UniSynth: Our algorithm for the quantitative problem has the following steps:
Calling UniDec. The algorithm calls UniDec, and if it returns “fail”, then return “fail”, otherwise execute the following steps. Obtain the following inequality from the transformation step of UniDec. 2. 2.
Variable Solving. The algorithm calculates for a given by e.g. repeatedly increasing (see Definition 4) and outputs the value of as the least number such that the following two conditions hold: (i) for all , we have (recall can be computed in linear time), and (ii) we have .
Theorem 4.3 (Soundness for UniSynth)
If the algorithm UniSynth outputs a real number , then is a univariate guess-and-check function for .
Example 12
Consider the recurrence relation for Sherwood’s Randomized-Search (cf. (2)) and . Consider that . From Example 9 and Example 10, the algorithm establishes the inequality and finds that . Then the algorithm finds through the followings: (a) ; (b) ; (c) ; (d) ; (e) . Thus, by Theorem 4.1, the expected running time of the algorithm has an upper bound . Later in Section 5, we show that one can obtain a much better through our algorithms by choosing , which is quite good since the optimal value lies in (cf. the first item R.-Sear. in Table 2).∎
4.2 Algorithm for Bivariate Recurrence Relations
In this part, we present our results for the separable bivariate recurrence relations. The key idea is to use separability to reduce the problem to univariate recurrence relations. There are two key steps which we describe below.
Step 1. The first step is to reduce a separable bivariate recurrence relation to a univariate one.
Definition 5 (From to )
Let be a separable bivariate recurrence relation taking the form (8). The univariate recurrence relation from is defined by eliminating any occurrence of and replacing any occurrence of with .
Informally, is obtained from by simply eliminating the roles of . The following example illustrates the situation for Coupon-Collector example.
Example 13
Consider to be the recurrence relation (9) for Coupon-Collector example. Then is as follows: and . ∎
Step 2. The second step is to establish the relationship between and , which is handled by the following proposition, whose proof is an easy induction on .
Proposition 6
For any separable bivariate recurrence relation taking the form (8), the solution is equal to .
Description of the Algorithm. With Proposition 6, the algorithm for separable bivariate recurrence relations is straightforward: simply compute for and then call the algorithms for univariate case presented in Section 4.1.
Analysis of examples in Section 2.4. Our algorithm can decide the following optimal bounds for the examples of Section 2.4.
For Example 6 we obtain an bound, whereas the worst-case bound is . 2. 2.
For Example 7 we obtain an bound for distributed setting and bound for concurrent setting, whereas the worst-case bounds are both .
Note that for all our examples, , and thus we obtain and upper bounds for expected-runtime analysis, which are the asymptotically optimal bounds. In all cases above, the worst-case analysis is completely ineffective as the worst-case bounds are infinite. Moreover, consider Example 7, where the optimal number of rounds is (i.e., one process every round, which centralized Round-Robin schemes can achieve). The randomized algorithm, with one shared variable, is a decentralized algorithm that achieves expected number of rounds (i.e., the optimal asymptotic expected-runtime complexity).
5 Experimental Results
We consider the classical examples illustrated in Section 2.2 and Section 2.4. In Table 2 for experimental results we consider the following recurrence relations : R.-Sear. corresponds to the recurrence relation (2) for Example 1; Q.-Sort corresponds to the recurrence relation (3) for Example 2; Q.-Select corresponds to the recurrence relation (4) for Example 3; Diam. A (resp. Diam. B) corresponds to the recurrence relation (5) (resp. the recurrence relation (6)) for Example 4; Sort-Sel. corresponds to recurrence relation (7) for Example 5, where we use the result from setting in Q.-Select; Coupon corresponds to the recurrence relation (9) for Example 6; Res. A (resp. Res. B) corresponds to the recurrence relation (10) (resp. the recurrence relation (11)) for Example 7.
In the table, specifies the input asymptotic bound, and Dec is the input which specifies either we use algorithm UniDec or the synthesis algorithm UniSynth with the given value, and gives the value synthesized w.r.t the given ( for yes). We describe below. We need approximation for constants such as and , and use the interval (resp., ) for tight approximation of (resp., ).
The value . For our synthesis algorithm we obtain the value . The optimal value of the associated constant with the asymptotic bound, denoted , is defined as follows. For , let ( is from (1)). Then the sequence is increasing in , and its limit is the optimal constant, i.e., . We consider as a lower bound on to compare against the value of we synthesize. In other words, is the minimal value such that (12) holds for , whereas for it must hold for all , and hence . Our experimental results show that the values we synthesize for is quite close to the optimal value.
We performed our experiments on Intel(R) Core(TM) i7-4510U CPU, 2.00GHz, 8GB RAM. All numbers in Table 2 are over-approximated up to , and the running time of all experiments are less than seconds. From Table 2, we can see that optimal are effectively over-approximated. For example, for Quick-Sort (Eq. (3)) (i.e, Q.-Sort in the table), our algorithm detects and the optimal one lies somewhere in . The experimental results show that we obtain the results extremely efficiently (less than -th of a second). For further details see Table 3 in Appendix 0.E.
6 Related Work
Automated program analysis is a very important problem with a long tradition [46]. The following works consider various approaches for automated worst-case bounds [28, 29, 30, 31, 32, 35, 34, 26, 5, 44] for amortized analysis, and the SPEED project [23, 24, 22] for non-linear bounds using abstract interpretation. All these works focus on the worst-case analysis, and do not consider expected-runtime analysis.
Our main contribution is automated analysis of recurrence relations. Approaches for recurrence relations have also been considered in the literature. Wegbreit [46] considered solving recurrence relations through either simple difference equations or generating functions. Zimmermann and Zimmermann [49] considered solving recurrence relations by transforming them into difference equations. Grobauer [21] considered generating recurrence relations from DML for the worst-case analysis. Flajolet et al. [19] considered allocation problems. Flajolet et al. [20] considered solving recurrence relations for randomization of combinatorial structures (such as trees) through generating functions. The COSTA project [2, 3, 4] transforms Java bytecode into recurrence relations and solves them through ranking functions. Moreover, The PURRS tool [6] addresses finite linear recurrences (with bounded summation), and some restricted linear infinite recurrence relations (with unbounded summation). Our approach is quite different because we consider analyzing recurrence relations arising from randomized algorithms and expected-runtime analysis through over-approximation of unbounded summations through integrals, whereas previous approaches either consider recurrence relations for worst-case bounds or combinatorial structures, or use generating functions or difference equations to solve the recurrence relations.
For intraprocedural analysis ranking functions have been widely studied [8, 9, 15, 42, 45, 17, 48, 43], which have then been extended to non-recursive probabilistic programs as ranking supermartingales [10, 18, 13, 12, 14, 11]. Such approaches are related to almost-sure termination, and not deriving optimal asymptotic expected-runtime bounds (such as , ).
Proof rules have also been considered for recursive (probabilistic) programs in [25, 33, 41], but these methods cannot be automated and require manual proofs.
7 Conclusion
In this work we considered efficient algorithms for automated analysis of randomized recurrences for logarithmic, linear, and almost-linear bounds. Our work gives rise to a number of interesting questions. First, an interesting theoretical direction of future work would be to consider more general randomized recurrence relations (such as with more than two variables, or interaction between the variables). While the above problem is of theoretical interest, most interesting examples are already captured in our class of randomized recurrence relations as mentioned above. Another interesting practical direction would be automated techniques to derive recurrence relations from randomized recursive programs.
Acknowledgements
We thank all reviewers for valuable comments. The research is partially supported by Vienna Science and Technology Fund (WWTF) ICT15-003, Austrian Science Fund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), the Natural Science Foundation of China (NSFC) under Grant No. 61532019 and the CDZ project CAP (GZ 1023).
Appendix 0.A Omitted Details for Section 2.2
Example 1. [Randomized-Search] Consider the Sherwood’s Randomized-Search algorithm (cf. [39, Chapter 9]) depicted in Fig. 1. The algorithm checks whether an integer value is present within the index range () in an integer array which is sorted in increasing order and is without duplicate entries. The algorithm outputs either the index for in or meaning that is not present in the index range of .
The description of the pseudo-code is as follows. The first four lines deal with the base case when there is only one index in the index range. The remaining lines deal with the recursive case: in line 6, an index is uniformly sampled from ; line 7–8 check whether is the output; line 9–12 perform the recursive calls depending on whether or not; finally, line 13–14 handle the case when or .
Let be the function such that for any , we have is the supremum of the expected execution times upon all inputs with . We derive a recurrence relation for as follows. Let and be any input such that . We clarify two cases below:
there exists an such that , where is interpreted here; 2. 2.
or .
In both cases, we have . In Case 1, we deduce from the pseudo-code in Fig. 1 that
[TABLE]
for all , where the maximum ranges over all ’s. In Case 2, similarly we deduce that
[TABLE]
Thus a preliminary version of the recurrence relation is and
[TABLE]
for all . Let be the unique solution to . Then from the fact that , by induction is monotonically increasing. Thus the maximum
[TABLE]
is attained at for all . Then is transformed into our final recurrence relation as follows:
[TABLE]
We note that the worst-case complexity for this algorithm is .∎
Example 2.[Quick-Sort] Consider the Quick-Sort algorithm [16, Chapter 7] depicted in Fig. 2, where every input is assumed to satisfy that and is an array of integers which does not contain duplicate numbers.
The description of the pseudo-code is as follows: first, line 2 samples an integer uniformly from ; then, line 3 calls a subroutine which (i) rearranges such that integers in which are less than come first, then , and finally integers in greater than , and (ii) outputs the new index of in ; and finally, lines 4–7 handle recursive calls to sub-arrays.
From the pseudo-code, the following recurrence relation is easily obtained:
[TABLE]
where represents the maximal expected execution time where is the array length and the execution time of pivoting is represented by . We note that the worst-case complexity for this algorithm is .∎
Example 3. [Quick-Select] Consider the Quick-Select algorithm (cf. [16, Chapter 9]) depicted in Fig. 4 which upon any input and such that , and contains no duplicate integers, finds the -th largest integer in . Note that for an array of size , and , we have the Median-Find algorithm.
The description of the pseudo-code is as follows: line 1 handles the base case; line 3 starts the recursive case by sampling uniformly from ; line 4 rearranges and returns an in the same way as in Quick-Sort (cf. Example 2); line 5 handles the case when happens to be the -th largest integer in ; and finally, line 7–10 handle the recursive calls.
Let be the function such that for any , we have is the supremum of the expected execution times upon all inputs with . By an analysis on where the -th largest integer lies in which is similar to the analysis on in Example 1, a preliminary recurrence relation is obtained such that and
[TABLE]
By similar monotone argument in Example 1, the maximum of the right-hand-side expression above is attained at for all . By the fact that for all , the following recurrence relation is obtained:
[TABLE]
To fit our univariate recurrence expression, we use over-approximation, and the final recurrence relation for this example is
[TABLE]
We note that the worst-case complexity for this algorithm is .∎
Example 4.[Diameter-Computation] Consider the Diameter-Computation algorithm (cf. [40, Chapter 9]) to compute the diameter of an input finite set of three-dimensional points. A pseudo-code to implement this is depicted in Fig. 4. The description of the pseudo-code is as follows: line 1–2 handle the base case; line 3 samples a point uniformly from ; line 4 calculates the maximum distance in from ; line 5 calculates the intersection of all balls centered at points in with uniform radius ; line 6 calculates the set of points outside ; lines 7–8 handle the situation which implies that is the diameter; lines 9–10 handle the recursive call to . Due to uniform choice of at line 3, the size of is uniformly in ; it then follows a pivoting (similar to that in Example 3 and Example 2) by line w.r.t the linear order over . Lines 5–6 can be done in time for Euclidean distance, and time for metric [40].
Depending on Eucledian or metric we obtain two different recurrence relations. For Eucledian we have the following relation:
[TABLE]
with the execution time for lines 5–6 being taken to be , and and for metric we have the following relation:
[TABLE]
with the execution time for lines 5–6 being taken to be . We note that the worst-case complexity for this algorithm is as follows: for Euclidean metric it is and for the metric it is .∎
Example 5.[Sorting with Quick-Select] Consider a sorting algorithm depicted in Fig. 5 which selects the median through the Quick-Select algorithm. The recurrence relation is directly obtained as follows:
[TABLE]
where is an upper bound on the expected running time of Quick-Select (cf. Example 3). We note that the worst-case complexity for this algorithm is .∎
Appendix 0.B Omitted Details for Section 2.4
Example 6.[Coupon-Collector] Consider the Coupon-Collector problem [40, Chapter 3] with different types of coupons (). The randomized process proceeds in rounds: at each round, a coupon is collected uniformly at random from the coupon types (i.e., each coupon type is collected with probability ); and the rounds continue until all the types of coupons are collected. We model the rounds as a recurrence relation with two variables , where represents the total number of coupon types and represents the remaining number of uncollected coupon types. The recurrence relation is as follows:
[TABLE]
where is the expected number of rounds, represents the expected number of rounds to collect a new (i.e., not-yet-collected) coupon type when there are still type of coupons to be collected, and (for ) represents the expected number of rounds to collect a new coupon type when there is only one new coupon type to be collected. We note that the worst-case complexity for this process is .∎
Example 7.[Channel-Conflict Resolution] We consider two network scenarios in which clients are trying to get access to a network channel. This problem is also called the Resource-Contention Resolution [36, Chapter 13]. In this problem, if more than one client tries to access the channel, then no client can access it, and if exactly one client requests access to the channel, then the request is granted. While centralized deterministic algorithms exist (such as Round-Robin) for the problem, to be implemented in a distributed or concurrent setting, randomized algorithms are necessary.
Distributed setting. In the distributed setting, the clients do not share any information. In this scenario, in each round, every client requests an access to the channel with probability . We are interested in the expected number of rounds until every client gets at least one access to the channel. At each round, let be the number of clients who have not got any access. Then the probability that a new client (from the clients) gets the access is . Thus, the expected rounds that a new client gets the access is . Since the sequence converges decreasingly to when , this expected time is no greater than . Then for this scenario, we obtain an over-approximating recurrence relation
[TABLE]
for the expected rounds until which every client gets at least one access to the channel. Note that in this setting no client has any information about any other client.
Concurrent setting. In the concurrent setting, the clients share one variable, which is the number of clients which has not yet been granted access. Also in this scenario, once a client gets an access the client does not request for access again. Moreover, the shared variable represents the number of clients that have not yet got access. In this case, in reach round a client that has not access to the channel yet, requests access to the channel with probability . Then the probability that a new client gets the access becomes . It follows that the expected time that a new client gets the access becomes which is smaller than . Then for this scenario, we obtain an over-approximating recurrence relation
[TABLE]
We also note that the worst-case complexity for both is .∎
Appendix 0.C Details for Overapproximations
To prove results for overapproximations for recurrence expressions, we need the following well-known theorem.
Theorem 0.C.1 (Taylor’s Theorem (with Lagrange’s Remainder) [7, Chapter 6])
For any function ( and ), if is ()-order differentiable, then for all , there exists a such that
[TABLE]
We also recall that
[TABLE]
where is the Apéry’s constant which lies in .
Moreover, we have the following result using integral-by-part technique and Newton-Leibniz Formula.
Lemma 2
For all such that , the following assertions hold:
[TABLE]
Furthermore, we need the following simple lemmas. The following lemma provides a tight approximation for floored expressions, the proof of which is a simple case distinction between even and odd cases.
Lemma 3
For all natural numbers , we have .
The following lemma handles over-approximation of simple summations.
Lemma 4
For any natural number and real number , one has that .
Then we prove the following two propositions.
Proposition 1. For any natural number , we have
[TABLE]
[TABLE]
Proof
Let be a natural number. The first argument comes from the facts that
[TABLE]
and
[TABLE]
where we use the fact that
[TABLE]
and is obtained from Taylor’s Theorem. The second argument comes from the facts that
[TABLE]
and
[TABLE]
where the first inequality is due to the fact that
[TABLE]
and is obtained from Taylor’s Theorem.∎
Proposition 2. For any natural number , we have
[TABLE]
Proof
The lemma follows directly from the fact that
[TABLE]
for some , which can be obtained through Taylor’s Theorem.∎
Proposition 3. For any natural number , we have:
[TABLE]
[TABLE]
[TABLE]
Proof
Let be a natural number such that . We first estimate the difference
[TABLE]
To this end, we deduce the following equalities:
[TABLE]
where is a real number in obtained from Taylor’s Theorem with Lagrange’s Remainder. The first and fourth equalities come from the linear property of Riemann Integral; the second one follows from the variable substitution ; the third one follows from Taylor’s Theorem. Using the fact that , one obtains that
[TABLE]
and
[TABLE]
Then (14) follows from the facts that
[TABLE]
and
[TABLE]
where in both situations we use the fact that for all .
Then we consider the difference
[TABLE]
First, we derive that
[TABLE]
where is a real number in obtained from Taylor’s Theorem. Using the fact that , one can obtain that
[TABLE]
where the second inequality follows from Inequality (18), and
[TABLE]
where the second inequality follows from Inequality (17). Then from Inequality (19) and Inequality (20), one has that
[TABLE]
and
[TABLE]
where in both situations we use the fact that for all . The inequalities above directly imply the inequalities in (15). Finally, we consider the difference
[TABLE]
Following similar approaches, we derive that for all natural numbers ,
[TABLE]
where . Thus, one obtains that
[TABLE]
and
[TABLE]
By plugging Inequalities in (18) and (20) into Inequality (21), one obtains that
[TABLE]
for all natural numbers . Similarly, by plugging Inequalities in (17) and (19) into Inequality (22), one obtains
[TABLE]
Then the inequalities in (16) are clarified.∎
Example 8. Consider the summation
[TABLE]
By Proposition 3, we can over-approximate it as
[TABLE]
which is equal to
[TABLE]
Then using Proposition 1, we can further obtain the following over-approximation
[TABLE]
which is roughly .∎
Appendix 0.D Proofs for Sect. 4.1
Lemma 1. Let and be a constant. For all univariate recurrence expressions , there exists pseudo-polynomials and such that coefficients (i.e., ’s in (13)) of are all non-negative, and the following assertion holds: for all and for all , with , the inequality is equivalent to .
Proof
From Definition 2, is a pseudo-polynomial. Simple rearrangement of terms in inequality gives the desired pseudo-polynomials. Moreover, the fact that all coefficients in (from (1)) are positive, is used to derive that all coefficients of are non-negative and .∎
Proposition 4. Let be pseudo-polynomials such that and all coefficients of are non-negative. Then there exists a real number such that for sufficiently large iff and .
Proof
We present the two directions of the proof.
(“If”:) Suppose that and . Then the result follows directly from the facts that (i) for sufficiently large and (ii) exists and is non-negative.
(“Only-if”:) Let be a positive real number such that for sufficiently large . Then , or otherwise is either constantly zero or negative for sufficiently large . Moreover, , since otherwise .∎
Proposition 5. Consider two univariate pseudo-polynomials such that , all coefficients of are non-negative and . Then given any ,
[TABLE]
for all (for of Definition 4).
Proof
Let be given in Definition 4. Fix an arbitrary and let be given in Definition 4. Then for all , (i) both are positive and (ii)
[TABLE]
and
[TABLE]
It follows that for all ,
[TABLE]
The desired result follows.∎
Theorem 4.2.[Soundness for UniDec] If UniDec outputs “yes”, then there exists a univariate guess-and-check function in form (12) for the inputs and . The algorithm is a linear-time algorithm in the size of the input recurrence relation.
Proof
From Definition 1 and the special form (12) for univariate guess-and-check functions, a function in form (12) which satisfies the inductive argument of Definition 1 can be modified to satisfy also the base condition of Definition 1 by simply raising to a sufficiently large amount. Then the correctness of the algorithm follows from Theorem 4.1 and the sufficiency of Proposition 4. Furthermore, the algorithm runs in linear time since the transformation from the inequality into (cf. Lemma 1) takes linear time in the size of the input recurrence relation. ∎
Theorem 4.3.[Soundness for UniSynth] If the algorithm UniSynth outputs a real number , then is a univariate guess-and-check function for .
Proof
Directly from the construction of the algorithm, Theorem 4.1, Proposition 4 and Proposition 5.∎
Appendix 0.E Detailed Experimental Results
The detailed experimental results are given in Table 3. We use to represent yes and for fail. In addition to Table 2, we include values for in Definition 4. For the separable bivariate examples, recall that does not change, and in these examples, the reduction to the univariate case is the function of .
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Akra, M.A., Bazzi, L.: On the solution of linear recurrence equations. Comp. Opt. and Appl. 10(2), 195–210 (1998), http://dx.doi.org/10.1023/A:1018373005182
- 2[2] Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G., Ramírez-Deantes, D.V., Román-Díez, G., Zanardini, D.: Termination and cost analysis with COSTA and its user interfaces. Electr. Notes Theor. Comput. Sci. 258(1), 109–121 (2009), http://dx.doi.org/10.1016/j.entcs.2009.12.008
- 3[3] Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings. Lecture Notes in Computer Science, vol. 5079, pp. 221–237. Springer (2008), http://dx.doi.org/10.1007/978-3-540-69166-2_15
- 4[4] Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of java bytecode. In: Nicola, R.D. (ed.) Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4421, pp. 157–172. Springer (2007), http://dx.doi.org/10.1007/978-3-540-71316-6_12
- 5[5] Avanzini, M., Lago, U.D., Moser, G.: Analysing the complexity of functional programs: higher-order meets first-order. In: Fisher, K., Reppy, J.H. (eds.) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015. pp. 152–164. ACM (2015), http://doi.acm.org/10.1145/2784731.2784753
- 6[6] Bagnara, R., , Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: Towards computer algebra support for fully automatic worst-case complexity analysis. Technical report, University of Parma (2005), https://arxiv.org/abs/cs/0512056
- 7[7] Bartle, R.G., Sherbert, D.R.: Introduction to Real Analysis. John Wiley & Sons, Inc., 4th edn. (2011)
- 8[8] Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: RTA. pp. 323–337 (2005)
