Decalf: A Directed, Effectful Cost-Aware Logical Framework
CoRR(2023)
摘要
We present decalf, a directed, effectful cost-aware logical framework for studying
quantitative aspects of functional programs with effects. Like calf,
the language is based on a formal phase distinction between the extension and
the intension of a program, its pure behavior as distinct from its cost
measured by an effectful step-counting primitive. The type theory ensures that
the behavior is unaffected by the cost accounting. Unlike calf, the
present language takes account of effects, such as probabilistic choice and
mutable state; this extension requires a reformulation of calf's
approach to cost accounting: rather than rely on a "separable" notion of cost,
here a cost bound is simply another program. To make this formal, we equip
every type with an intrinsic preorder, relaxing the precise cost accounting
intrinsic to a program to a looser but nevertheless informative estimate. For
example, the cost bound of a probabilistic program is itself a probabilistic
program that specifies the distribution of costs. This approach serves as a
streamlined alternative to the standard method of isolating a recurrence that
bounds the cost in a manner that readily extends to higher-order, effectful
programs.
The development proceeds by first introducing the decalf type system,
which is based on an intrinsic ordering among terms that restricts in the
extensional phase to extensional equality, but in the intensional phase
reflects an approximation of the cost of a program of interest. This
formulation is then applied to a number of illustrative examples, including
pure and effectful sorting algorithms, simple probabilistic programs, and
higher-order functions. Finally, we justify decalf via a model in the
topos of augmented simplicial sets.
更多查看译文
关键词
algorithm analysis,amortized analysis,behavioral verification,cost models,equational reasoning,intensional property,mechanized proof,modal type theory,noninterference,parallel algorithms,phase distinction,proof assistants,recurrence relations
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要