A type theory for incremental computational complexity with control flow changes
A type theory for incremental computational complexity with control flow changes
复制标题
随控制流变化而增加计算复杂性的类型理论
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
D. Garg
中科院分区：
文献类型：
--
作者：
Ezgi Çiçek;Zoe Paraskevopoulou;D. Garg
增量计算旨在稍微修改其输入后加快程序的重新运行。它可以通过记录程序的第一次运行的痕迹并通过痕量进行增量运行，并试图重新利用尽可能多的原始跟踪。最近的工作Costit是一种类型和效果系统，可以确定程序的增量运行的时间复杂性，以作为输入更改的函数。但是，Costit在两种方面受到限制。首先，它禁止影响控制流的输入变化。这使得不可能输入程序，例如，在可能会更改的输入上分支。其次，相对于抽象成本语义，证明了Costit的健全性，但目前尚不清楚如何实现语义。在本文中，我们解决了这两个限制。我们提出了DucoStit，这是Costit的重新设计，结合了关于变更传播成本和划痕评估成本的推理。后者增加了对控制流动的限制。为了获得类型系统，我们完善了流程CAML，这是一种用于信息流量分析的类型系统，具有成本效果。此外，我们从Costit索引的细化中继承了跟踪数据结构大小和共同构型类型。使用二进制和一级步骤指数逻辑关系的结合，我们证明了杜科斯蒂特的成本分析不仅相对于抽象成本语义，而且还相对于具体语义，这是通过翻译成ML样语言而获得的。
Incremental computation aims to speed up re-runs of a program after its inputs have been modified slightly. It works by recording a trace of the program's first run and propagating changes through the trace in incremental runs, trying to re-use as much of the original trace as possible. The recent work CostIt is a type and effect system to establish the time complexity of incremental runs of a program, as a function of input changes. However, CostIt is limited in two ways. First, it prohibits input changes that influence control flow. This makes it impossible to type programs that, for instance, branch on inputs that may change. Second, the soundness of CostIt is proved relative to an abstract cost semantics, but it is unclear how the semantics can be realized. In this paper, we address both these limitations. We present DuCostIt, a re-design of CostIt, that combines reasoning about costs of change propagation and costs of from-scratch evaluation. The latter lifts the restriction on control flow changes. To obtain the type system, we refine Flow Caml, a type system for information flow analysis, with cost effects. Additionally, we inherit from CostIt index refinements to track data structure sizes and a co-monadic type. Using a combination of binary and unary step-indexed logical relations, we prove DuCostIt's cost analysis sound relative to not only an abstract cost semantics, but also a concrete semantics, which is obtained by translation to an ML-like language.