一句话：以指称语义形式化函数式程序的代价递推提取：先用单子翻译提取代价，再借不同模型刻画不同的规模概念。
分析函数式程序渐近复杂度通常依赖非形式方法：先提取以输入规模为参数的代价递推，再求闭式上界，但缺少形式语义基础。本文针对带 let-多态的高阶函数式语言给出该方法的正式刻画，分两阶段：先用单子翻译把原程序转成带代价注解的程序，再把提取结果在模型中解释，模型的选择决定“规模”的含义。对归纳类型参数，不同分析适用不同的规模概念；对多态函数，可用各类型实例规模概念的公共数据形式地刻画参数规模的语义。作者给出若干模型实例，形式化地论证多种非形式代价分析，展示方法的适用性。
Abstract A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input and then to compute a closed-form upper bound on that recurrence. We give a formal account of that method for functional programs in a higher order language with $\mathtt{let}$ -polymorphism. The method consists of two phases. In the first phase, a monadic translation is performed to extract a cost-annotated version of the original program. In the second phase, the extracted program is interpreted in a model. The key feature of this second phase is that different models describe different notions of size. This plays out in several ways. For example, when analyzing functions that take arguments of inductive types, different notions of size may be appropriate depending on the analysis. When analyzing polymorphic functions, our approach shows that one can formally describe the notion of size of an argument in terms of the data that is common to the notions of size for each type instance of the domain type. We give several examples of different models that formally justify various informal cost analyses to show the applicability of our approach.
@article{paperbot1631,
title = {Denotational semantics as a foundation for cost recurrence extraction for functional languages},
author = {NORMAN DANNER and DANIEL R. LICATA},
journal = {Journal of Functional Programming},
volume = {32},
year = {2022},
doi = {10.1017/s095679682200003x}
}