内终止性和导数复杂性的解卷积
Uncurrying for Innermost Termination and Derivational Complexity
摘要：
一阶应用项重写系统为高阶方面建模提供了一个自然的框架。在早期的工作中，我们介绍了一个uncurrying变换，这是终止保持和反射。在本文中，我们将探讨这种转换的行为最内层终止和（最内层）派生复杂性。我们证明了它反映了最内终止性和最内导复杂性，并保持和反映了多项式导复杂性。为了保持最内层终止性和最内层导子复杂性，我们给出了反例。因此，解卷积可以用作最内层终止证明的预处理变换，并建立推导复杂性的多项式上界和下界。此外，它可以用来建立上界的最内层的衍生复杂性，而它既不是健全的证明最内层的非终止性，也不是获得下界的最内层的衍生复杂性。
英文摘要：
First-order applicative term rewriting systems provide a natural framework for modeling higher-order aspects. In earlier work we introduced an uncurrying transformation which is termination preserving and reflecting. In this paper we investigate how this transformation behaves for innermost termination and (innermost) derivational complexity. We prove that it reflects innermost termination and innermost derivational complexity and that it preserves and reflects polynomial derivational complexity. For the preservation of innermost termination and innermost derivational complexity we give counterexamples. Hence uncurrying may be used as a preprocessing transformation for innermost termination proofs and establishing polynomial upper and lower bounds on the derivational complexity. Additionally it may be used to establish upper bounds on the innermost derivational complexity while it neither is sound for proving innermost non-termination nor for obtaining lower bounds on the innermost derivational complexity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
