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.
翻译:摘要: 在重写中,时间复杂度自然地被理解为将术语约减到标准形式所需的步骤数。确立此措施的复杂性限制是重写社区中已知的问题。发现此类限制的绝大多数技术都包括修改终止证明以恢复复杂性信息。这已经在语义解释、递归路径序和依赖对等方面完成。在本文中,我们按照相同的方案,通过定制元组解释来处理最内部的复杂性分析。元组解释将术语解释为保持减少成本和正常形式大小的上限的元组。与完整的重写环境不同,当减少是最内层的时,强单调成本组件要求会被放弃。这个减少对成本元组的弱化要求使我们能够证明兼容系统最内部的重写关系是良基础的。我们建立了元组解释保证兼容系统的运行时多项式限制的必要条件,并描述了这种解释的搜索程序。