论文标题
表示语义作为功能语言的成本复发提取的基础
Denotational semantics as a foundation for cost recurrence extraction for functional languages
论文作者
论文摘要
分析程序的渐近复杂性的一种标准非正式方法是提取复发性，该复发是根据其输入的大小来描述其成本，然后计算该复发的封闭形式的上限。我们对使用LET-Polymormorlist的高阶语言的功能程序进行正式描述。该方法由两个阶段组成。在第一阶段，进行了单调的翻译以提取原始程序的成本宣布版本。在第二阶段，提取的程序在模型中被解释。第二阶段的关键特征是不同的模型描述了不同的大小概念。这有几种方式。例如，当分析采用归纳类型参数的函数时，根据分析，不同的大小概念可能是适当的。在分析多态性函数时，我们的方法表明，可以正式描述参数大小的概念，这些数据是域类型的每个类型实例的大小概念的数据。我们给出了几个不同模型的例子，这些示例正式证明了各种非正式成本分析以显示我们方法的适用性。
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 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.
