依赖类型 AARA：高阶程序资源分析的非仿射方法

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