2006/08/03 by Jean-Yves Marion, Romain Péchoux, Marion, Jean-Yves +2
Computer Science · #Computational Complexity (cs.CC) #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #cs.CC
paper · pdf · doi:10.48550/arxiv.cs/0608020
arxiv created 2006/08/03 · openalex publication_date 2006/08/03 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In a previous paper, the sup-interpretation method was proposed as a new tool to control memory resources of first order functional programs with pattern matching by static analysis. Basically, a sup-interpretation provides an upper bound on the size of function outputs. In this former work, a criterion, which can be applied to terminating as well as non-terminating programs, was developed in order to bound polynomially the stack frame size. In this paper, we suggest a new criterion which captures more algorithms computing values polynomially bounded in the size of the inputs. Since this work is related to quasi-interpretations, we compare the two notions obtaining two main features. The first one is that, given a program, we have heuristics for finding a sup-interpretation when we consider polynomials of bounded degree. The other one consists in the characterizations of the set of function computable in polynomial time and in polynomial space.