A unifying type-theory for higher-order (amortized) cost analysis
A unifying type-theory for higher-order (amortized) cost analysis
复制标题
高阶（摊销）成本分析的统一类型理论
DOI：
10.1145/3434308
复制
发表时间：
2021
影响因子：
--
通讯作者：
Hoffmann, Jan
中科院分区：
文献类型：
--
作者：
Rajani, Vineet;Gaboardi, Marco;Garg, Deepak;Hoffmann, Jan
本文提出了一种新的用于高阶函数式程序摊销成本分析的类型论框架λ-AMOR，并证明了现有的类型成本分析系统可以嵌入到该框架中。λ-AMOR引入了一种新的模式类型来表示潜在成本-已经核算但尚未发生的成本，这是摊销分析的核心。此外，λ-AMOR依赖于标准的类型论概念，如亲和性、精化类型和指数化成本单体。λ-AMOR用一个相当简单的逻辑关系被证明是正确的。我们在λ-AMOR中嵌入了两个现有的成本分析系统，表明尽管λ-AMOR很简单，但它可以模拟不同评估策略(按名称和按价值调用)、不同风格(基于效果和基于协同影响)以及有或没有摊销的成本分析。其中一个嵌入还意味着λ-AMOR对于所有终止的PCF程序是相对完整的。
This paper presents λ-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it. λ-amor introduces a new modal type for representing potentials – costs that have been accounted for, but not yet incurred, which are central to amortized analysis. Additionally, λ-amor relies on standard type-theoretic concepts like affineness, refinement types and an indexed cost monad. λ-amor is proved sound using a rather simple logical relation. We embed two existing type systems for cost analysis in λ-amor showing that, despite its simplicity, λ-amor can simulate cost analysis for different evaluation strategies (call-by-name and call-by-value), in different styles (effect-based and coeffect-based), and with or without amortization. One of the embeddings also implies that λ-amor is relatively complete for all terminating PCF programs.
登录
查看更多内容
通过分级结合效应和协同效应
DOI：
10.1145/2951913.2951939
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Gaboardi M
通讯作者：
Gaboardi M
DOI：
10.1137/0606031
发表时间：
1985-04
期刊：
Siam Journal on Algebraic and Discrete Methods
影响因子：
--
作者：
R. Tarjan
通讯作者：
R. Tarjan
通过协同效应按需调用效果
影响因子：
1.5
作者：
McDermott D
通讯作者：
McDermott D
通过按值调用对功能程序进行递归提取
DOI：
--
发表时间：
2019
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
G. A. Kavvos;Edward Morehouse;Daniel R. Licata;N. Danner
通讯作者：
N. Danner
协同效应
DOI：
--
发表时间：
2014
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
T. Petříček;Dominic A. Orchard;A. Mycroft
通讯作者：
A. Mycroft