Static resource analysis determines the resource consumption (e.g., time complexity) of a program without executing it. Among the numerous existing approaches for resource analysis, affine type systems have been one dominant approach. However, these affine type systems fall short of deriving precise resource behavior of higher-order programs, particularly in cases that involve partial applications. This article presents λ_\ms{amor}^\ms{na}}, a non-affine AARA-style dependent type system for resource reasoning about higher-order functional programs. The key observation is that the main issue in previous approaches comes from (i) the close coupling of types and resources, and (ii) the conflict between affine and higher-order typing mechanisms. To derive precise resource behavior of higher-order functions, λ_\ms{amor}^\ms{na}} decouples resources from types and follows a non-affine typing mechanism. The non-affine type system of λ_\ms{amor}^\ms{na}} achieves this by using dependent types, which allows expressing type-level potential functions separate from ordinary types. This article formalizes λ_\ms{amor}^\ms{na}}'s syntax and semantics, and proves its soundness, which guarantees the correctness of resource bounds. Several challenging classic and higher-order examples are presented to demonstrate the expressiveness and compositionality of λ_\ms{amor}^\ms{na}}'s reasoning capability.

翻译：静态资源分析在不执行程序的情况下确定其资源消耗（例如，时间复杂度）。在现有的众多资源分析方法中，仿射类型系统一直是主流方法之一。然而，这些仿射类型系统难以推导高阶程序的精确资源行为，尤其是在涉及部分应用的情况下。本文提出 λ_\ms{amor}^\ms{na}}，一种用于高阶函数程序资源推理的非仿射AARA风格依赖类型系统。关键观察是，先前方法的主要问题源于（i）类型与资源的紧密耦合，以及（ii）仿射与高阶类型机制之间的冲突。为了推导高阶函数的精确资源行为，λ_\ms{amor}^\ms{na}} 将资源与类型解耦，并遵循非仿射的类型机制。λ_\ms{amor}^\ms{na}} 的非仿射类型系统通过使用依赖类型实现这一点，这使得能够表达独立于普通类型的类型级势函数。本文形式化了 λ_\ms{amor}^\ms{na}} 的语法和语义，并证明了其可靠性，从而保证了资源界限的正确性。文中给出了几个具有挑战性的经典和高阶示例，以展示 λ_\ms{amor}^\ms{na}} 推理能力的表达性和组合性。