Certifying polynomial time and linear/polynomial space for imperative programs
In earlier work of Kristiansen and Niggl the polynomial-time computable functions were characterized by stack programs of mu-measure 0, and the linear-space computable functions by loop programs of mu-measure 0. Until recently, an open problem was how to extend these characterizations to programs with user-friendly basic instructions, such as assignment statements, and with mixed data structures. It is shown how to strengthen the above characterizations to imperative programs built from arbitrary basic instructions by sequencing and by if-then-else and for-do statements. These programs operate on variables, each of which may represent any data structure such as stacks, registers, trees, or graphs. The paper presents a new method of certifying "polynomial size boundedness" of such imperative programs under the natural assumption that the basic instructions used are polynomially size bounded, too. The certificate for a program P with variables among X-1,...,X-n will be an (n+1) x (n+1) matrix M(P) over the finite set {0, 1,infinity}. It is shown that certified string programs (i.e., stack programs, but with any polynomial-time computable basic instructions) exactly compute the functions in FPTIME. Accordingly, certified general loop programs (using any linear-space computable basic instructions) exactly compute the functions in FLINSPACE. Furthermore, it is shown that certified power string programs (i.e., string programs, but built from polynomial-space computable basic instructions and extended by power loop statements) exactly compute the polynomial-space computable functions in FPSPACE. In addition, examples of certified "natural" (implementations of) algorithms, such as insertion-sort or binary addition and multiplication, are given.
polynomial time polynomial space linear space static program analysis property testing implicit computational complexity imperative programming languages