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.

翻译：在重写系统中，时间复杂度自然理解为将项归约为范式所需的步数。为该度量建立复杂度边界是重写领域的一个经典问题。大多数寻找此类边界的技术涉及修改终止性证明以恢复复杂度信息，例如通过语义解释、递归路径序和依赖对等方法。本文遵循相同思路，通过调整元组解释来处理最内复杂度分析。元组解释将项解释为包含归约代价上界和范式规模上界的元组。与完全重写设置不同，当归约为最内层时，代价分量不再要求强单调性。代价元组这一弱化条件使我们能够证明兼容性结果的最内版本：若项重写系统中的所有规则可被严格定向，则最内重写关系是良基的。我们建立了元组解释保证兼容系统运行时多项式边界的必要条件，并描述了此类解释的搜索过程。