Complexity Hierarchies and Higher-Order Cons-Free Rewriting

Authors Cynthia Kop, Jakob Grue Simonsen

Thumbnail PDF


  • Filesize: 0.6 MB
  • 18 pages

Document Identifiers

Author Details

Cynthia Kop
Jakob Grue Simonsen

Cite AsGet BibTex

Cynthia Kop and Jakob Grue Simonsen. Complexity Hierarchies and Higher-Order Cons-Free Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the computational intuition is that rules cannot build new data structures. It is well-known that cons-free programming languages can be used to characterize computational complexity classes, and that cons-free first-order term rewriting can be used to characterize the set of polynomial-time decidable sets. We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the order of the types used in the systems. We prove that, for every k >= 1, left-linear cons-free systems with type order k characterize E^kTIME if arbitrary evaluation is used (i.e., the system does not have a fixed reduction strategy). The main difference with prior work in implicit complexity is that (i) our results hold for non-orthogonal term rewriting systems with possible rule overlaps with no assumptions about reduction strategy, (ii) results for such term rewriting systems have previously only been obtained for k = 1, and with additional syntactic restrictions on top of cons-freeness and left-linearity. Our results are apparently among the first implicit characterizations of the hierarchy E^1TIME != E^2TIME != .... Our work confirms prior results that having full non-determinism (via overlaps of rules) does not directly allow for characterization of non-deterministic complexity classes like NE. We also show that non-determinism makes the classes characterized highly sensitive to minor syntactic changes such as admitting product types or non-left-linear rules.
  • higher-order term rewriting
  • implicit complexity
  • cons-freeness
  • ETIME hierarchy


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. M. Avanzini, N. Eguchi, and G. Moser. A new order-theoretic characterisation of the polytime computable functions. In APLAS, volume 7705 of LNCS, pages 280-295, 2012. URL:
  2. M. Avanzini and G. Moser. Closing the gap between runtime complexity and polytime computability. In RTA, volume 6 of LIPIcs, pages 33-48, 2010. URL:
  3. M. Avanzini and G. Moser. Polynomial path orders. LMCS, 9(4), 2013. URL:
  4. P. Baillot. From proof-nets to linear logic type systems for polynomial time computing. In TLCA, volume 4583 of LNCS, pages 2-7, 2007. URL:
  5. P. Baillot, M. Gaboardi, and V. Mogbil. A polytime functional language from light linear logic. In ESOP, volume 6012 of LNCS, pages 104-124, 2010. URL:
  6. P. Baillot and U. Dal Lago. Higher-Order Interpretations and Program Complexity. In CSL, volume 16 of LIPIcs, pages 62-76, 2012. URL:
  7. S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity, 2:97-110, 1992. URL:
  8. S. Bellantoni, K. Niggl, and H. Schwichtenberg. Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic, 104(1-3):17-30, 2000. URL:
  9. F. Blanqui, J. Jouannaud, and A. Rubio. The computability path ordering: The end of a quest. In CSL, volume 5213 of LNCS, pages 1-14, 2008. Google Scholar
  10. G. Bonfante. Some programming languages for logspace and ptime. In AMAST, volume 4019 of LNCS, pages 66-80, 2006. URL:
  11. D. de Carvalho and J. Simonsen. An implicit characterization of the polynomial-time decidable sets by cons-free rewriting. In RTA-TLCA, volume 8560 of LNCS, pages 179-193, 2014. Google Scholar
  12. M. Hofmann. Type systems for polynomial-time computation, 1999. Habilitationsschrift. Google Scholar
  13. N. Jones. Computability and Complexity from a Programming Perspective. MIT Press, 1997. Google Scholar
  14. N. Jones. The expressive power of higher-order types or, life without CONS. JFP, 11(1):55-94, 2001. Google Scholar
  15. J. Jouannaud and A. Rubio. The higher-order recursive path ordering. In LICS, pages 402-411, 1999. Google Scholar
  16. C. Kop and J. Simonsen. Complexity hierarchies and higher-order cons-free rewriting (extended version). Technical report, University of Copenhagen, 2016. Available online at the authors' homepages. Google Scholar
  17. L. Kristiansen and K. Niggl. On the computational complexity of imperative programming languages. TCS, 318(1-2):139-161, 2004. URL:
  18. R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. TCS, 192(1):3-29, 1998. Google Scholar
  19. C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. Google Scholar
  20. M. Sipser. Introduction to the Theory of Computation. Thomson Course Technology, 2006. Google Scholar
  21. F. van Raamsdonk. Higher-order rewriting. In Term Rewriting Systems, Chapter 11. Cambridge University Press, 2003. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail