10.1145/3339984
Chatterjee, Krishnendu
Krishnendu
Chatterjee0000-0002-4561-241X
Fu, Hongfei
Hongfei
Fu
Goharshady, Amir Kafshdar
Amir Kafshdar
Goharshady0000-0003-1702-6584
Non-polynomial worst-case analysis of recursive programs
ACM
2019
2019-11-13T08:33:43Z
2020-01-17T09:52:21Z
journal_article
https://research-explorer.app.ist.ac.at/record/7014
https://research-explorer.app.ist.ac.at/record/7014.json
1705.00317
We study the problem of developing efficient approaches for proving
worst-case bounds of non-deterministic recursive programs. Ranking functions
are sound and complete for proving termination and worst-case bounds of
nonrecursive programs. First, we apply ranking functions to recursion,
resulting in measure functions. We show that measure functions provide a sound
and complete approach to prove worst-case bounds of non-deterministic recursive
programs. Our second contribution is the synthesis of measure functions in
nonpolynomial forms. We show that non-polynomial measure functions with
logarithm and exponentiation can be synthesized through abstraction of
logarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem
using linear programming. While previous methods obtain worst-case polynomial
bounds, our approach can synthesize bounds of the form $\mathcal{O}(n\log n)$
as well as $\mathcal{O}(n^r)$ where $r$ is not an integer. We present
experimental results to demonstrate that our approach can obtain efficiently
worst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the
divide-and-conquer algorithm for the Closest-Pair problem, where we obtain
$\mathcal{O}(n \log n)$ worst-case bound, and (ii) Karatsuba's algorithm for
polynomial multiplication and Strassen's algorithm for matrix multiplication,
where we obtain $\mathcal{O}(n^r)$ bound such that $r$ is not an integer and
close to the best-known bounds for the respective algorithms.