Non-polynomial worst-case analysis of recursive programs
Chatterjee, Krishnendu
Fu, Hongfei
Goharshady, Amir Kafshdar
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.
ACM
2019
info:eu-repo/semantics/article
doc-type:article
text
https://research-explorer.app.ist.ac.at/record/7014
Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href="https://doi.org/10.1145/3339984">10.1145/3339984</a>
eng
info:eu-repo/semantics/altIdentifier/doi/10.1145/3339984
info:eu-repo/semantics/altIdentifier/arxiv/1705.00317
info:eu-repo/grantAgreement/EC/ICT15-003
info:eu-repo/grantAgreement/EC/S 11407_N23
info:eu-repo/grantAgreement/EC/FP7/279307
info:eu-repo/semantics/closedAccess