Analyzing Innermost Runtime Complexity Through Tuple Interpretations

Liye Guo
(Radboud University)
Deivid Vale
(Radboud University)

Time complexity in rewriting is naturally understood as the number of steps needed to reduce terms to normal forms. Establishing complexity bounds to this measure is a well-known problem in the rewriting community. A vast majority of techniques to find such bounds consist of modifying termination proofs in order to recover complexity information. This has been done for instance with semantic interpretations, recursive path orders, and dependency pairs. In this paper, we follow the same program by tailoring tuple interpretations to deal with innermost complexity analysis. A tuple interpretation interprets terms as tuples holding upper bounds to the cost of reduction and size of normal forms. In contrast with the full rewriting setting, the strongly monotonic requirement for cost components is dropped when reductions are innermost. This weakened requirement on cost tuples allows us to prove the innermost version of the compatibility result: if all rules in a term rewriting system can be strictly oriented, then the innermost rewrite relation is well-founded. We establish the necessary conditions for which tuple interpretations guarantee polynomial bounds to the runtime of compatible systems and describe a search procedure for such interpretations.

In Daniele Nantes-Sobrinho and Pascal Fontaine: Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications (LSFA 2022), Belo Horizonte, Brazil, 23-24 September 2022, Electronic Proceedings in Theoretical Computer Science 376, pp. 34–48.
Published: 23rd March 2023.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: