Amir M. Ben-Amram ; Geoff Hamilton - Tight Polynomial Worst-Case Bounds for Loop Programs

lmcs:5596 - Logical Methods in Computer Science, May 14, 2020, Volume 16, Issue 2 - https://doi.org/10.23638/LMCS-16(2:4)2020
Tight Polynomial Worst-Case Bounds for Loop ProgramsArticle

Authors: Amir M. Ben-Amram ; Geoff Hamilton

    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.


    Volume: Volume 16, Issue 2
    Published on: May 14, 2020
    Accepted on: April 11, 2020
    Submitted on: June 25, 2019
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,F.2.0,F.2.0

    Consultation statistics

    This page has been seen 1119 times.
    This article's PDF has been downloaded 355 times.