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.
翻译:用于分析一个程序无症状复杂性的标准非正式方法是,从输入量大小的角度,提取一个描述其成本的重现,然后根据该重现计算一个封闭式的上限。我们用一个高阶语言,用顺向多形态主义的方式,正式描述该功能程序的方法。该方法由两个阶段组成。在第一阶段,进行一个monadic翻译,以提取原始程序的成本附加说明版本。在第二阶段,提取的程序在一个模型中解释。第二阶段的关键特征是不同的模型描述不同的规模概念。这以几种方式出现。例如,在分析从缩入类型的角度分析功能时,不同规模的概念可能适合分析。在分析多形态函数时,我们的方法表明,可以正式描述与每个类型域类型大小概念共同的数据的大小概念。我们举出了不同模型的几种例子,正式证明各种非正式成本分析可以显示我们方法的可适用性。