The strength of non-size increasing computation

ABSTRACT

We study the expressive power of non-size increasing recursive definitions over lists. This notion of computation is such that the size of all intermediate results will automatically be bounded by the size of the input so that the interpretation in a finite model is sound with respect to the standard semantics. Many well-known algorithms with this property such as the usual sorting algorithms are definable in the system in the natural way. The main result is that a characteristic function is definable if and only if it is computable in time O(2^p(n)) for some polynomial p.The method used to establish the lower bound on the expressive power also shows that the complexity becomes polynomial time if we allow primitive recursion only. This settles an open question posed in [1, 7].The key tool for establishing upper bounds on the complexity of derivable functions is an interpretation in a finite relational model whose correctness with respect to the standard interpretation is shown using a semantic technique.

REFERENCES

• 1: Klaus Aehlig , Helmut Schwichtenberg, A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.84, June 26-29, 2000
• 2: Henry G. Baker, Lively linear Lisp: “look ma, no garbage!”, ACM SIGPLAN Notices, v.27 n.8, p.89-98, Aug. 1992 [doi>10.1145/142137.142162]
• 3: Stephen Bellantoni , Stephen Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity, v.2 n.2, p.97-110, 1992 [doi>10.1007/BF01201998]
• 4: Vuokko-Helema Caseiro. Equations for Defining Poly-time Functions. PhD thesis, Umiversity of Oslo, 1997. Available by ftp flom ftp. ifi. uio. no/pub/vuokko/Oadm, ps.
• 5: Stephen A. Cook. Linear-time simulation of deterministic two-way pushdown automata. Information PTvcessing, 71:75-80, 1972.
• 6: Andreas Goerdt, Characterizing complexity classes by higher type primitive recursive definitions, Theoretical Computer Science, v.100 n.1, p.45-66, June 22, 1992 [doi>10.1016/0304-3975(92)90363-K]
• 7: Martin Hofmann, Linear Types and Non Size-Increasing Polynomial Time Computation, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.464, July 02-05, 1999
• 8: Martin Hofmann, A type system for bounded space and functional in-place update, Nordic Journal of Computing, v.7 n.4, p.258-289, Winter 2000
• 9: Neil D. Jones, The expressive power of higher-order types or, life without CONS, Journal of Functional Programming, v.11 n.1, p.55-94, January 2001 [doi>10.1017/S0956796800003889]
• 10: Daniel Leivant, Stratified functional programs and computational complexity, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.325-333, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158659]
• 11: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 1993

INDEX TERMS

Keywords:
computational complexity, finite model, higher-order functions, semantics