A flow calculus of mwp-bounds for complexity analysis

TY - JOUR

T1 - A flow calculus of mwp-bounds for complexity analysis

AU - Jones, Neil

AU - Kristiansen, Lars

PY - 2009/8/1

Y1 - 2009/8/1

N2 - We present a method for certifying that the values computed by an imperative program will be bounded by polynomials in the program's inputs. To this end, we introduce mwp-matrices and define a semantic relation C : M, where C is a program and M is an mwp-matrix. It follows straightforwardly from our definitions that there exists M such that C : M holds iff every value computed by C is bounded by a polynomial in the inputs. Furthermore, we provide a syntactical proof calculus and define the relation ⊢ C : M to hold iff there exists a derivation in the calculus where C : M is the bottom line. We prove that ⊢ C : M implies C : M. By means of exhaustive proof search, an algorithm can decide if there exists M such that the relation ⊢ C : M holds, and thus, our results yield a computational method.

AB - We present a method for certifying that the values computed by an imperative program will be bounded by polynomials in the program's inputs. To this end, we introduce mwp-matrices and define a semantic relation C : M, where C is a program and M is an mwp-matrix. It follows straightforwardly from our definitions that there exists M such that C : M holds iff every value computed by C is bounded by a polynomial in the inputs. Furthermore, we provide a syntactical proof calculus and define the relation ⊢ C : M to hold iff there exists a derivation in the calculus where C : M is the bottom line. We prove that ⊢ C : M implies C : M. By means of exhaustive proof search, an algorithm can decide if there exists M such that the relation ⊢ C : M holds, and thus, our results yield a computational method.

U2 - 10.1145/1555746.1555752

DO - 10.1145/1555746.1555752

M3 - Journal article

SN - 1529-3785

VL - 10

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 4

M1 - 28

ER -