AI 中文总结
该研究提出算子语义与抽象编译框架，将其应用于静态代价分析，开发出支持通用函数未知量等的最优递归提取技术，提升了代价分析的可靠性与精确性。
AI 中文摘要
最小不动点是程序语义的基础，但它们会抽象掉生成它们的递归结构。我们引入算子语义：一种介于语法和经典指称语义之间的语义中间表示，将程序视为算子。抽象编译随后被理解为对这类算子进行抽象的行为。我们为函数、算子和程序本身开发了高阶抽象域，其中组合是关键的新原语，同时还有一个用于构建可靠、精确且模块化的抽象编译器的范畴框架。我们在基于递归的静态代价分析背景下实例化该框架，为代数数据类型上的递归程序开发了与求解器无关的最优递归提取技术，该技术支持通用函数未知量和泛化变形度量，这是一类超越传统方法的广泛规模度量。
英文摘要
Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate representation between syntax and classical denotational semantics, which treats programs as operators. Abstract compilation is then understood as the act of abstracting such operators. We develop higher-order abstract domains for functions, operators, and programs themselves, in which composition is the key novel primitive, together with a categorical framework for constructing sound, precise, and modular abstract compilers. We instantiate this framework in the context of recurrence-based static cost analysis, developing solver-independent, optimal recurrence extraction techniques for recursive programs over algebraic data types, that support general function unknowns and catamorphic metrics, a broad class of size metrics beyond traditional approaches.
