Tight Polynomial Worst-Case Bounds for Loop Programs
2020
In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple
programming language - representing non-deterministic imperative programs with
bounded loops, and arithmetics limited to addition and multiplication - it is
possible to decide precisely whether a program has certain growth-rate
properties, in particular whether a computed value, or the program's running
time, has a polynomial growth rate.
A natural and intriguing problem was to move from answering the decision
problem to giving a quantitative result, namely, a tight polynomial upper
bound. This paper shows how to obtain asymptotically-tight, multivariate,
disjunctive polynomial bounds for this class of programs. This is a complete
solution: whenever a polynomial bound exists it will be found.
A pleasant surprise is that the algorithm is quite simple; but it relies on
some subtle reasoning. An important ingredient in the proof is the forest
factorization theorem, a strong structural result on homomorphisms into a
finite monoid.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI