指称语义作为功能型语言的成本循环提取基础
摘要：用于分析程序渐近复杂性的标准非正式方法是提取一个递归关系，该关系描述其成本与输入的大小成正比，然后计算该递归关系的闭合上界。我们在具有let多态性的高阶语言中给出了该方法的正式描述。该方法包括两个阶段。在第一个阶段中，执行一个单子化翻译，以提取原始程序的成本注释版本。在第二个阶段中，通过模型解释提取的程序。此第二阶段的关键特点是不同的模型描述不同的大小概念。这在多个方面有所体现。例如，当分析接受归纳类型参数的函数时，根据分析的不同，不同的大小概念可能合适。在分析多态函数时，我们的方法表明可以形式上描述参数的大小概念，其中描述了该域类型每个类型实例的大小概念共有的数据。我们给出了几个不同的模型示例，以形式上证明各种非正式成本分析的适用性。
作者：Norman Danner and Daniel R. Licata
论文ID：2002.07262
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-08-09