We present ${\bf decalf}$, a ${\bf d}$irected, ${\bf e}$ffectful ${\bf c}$ost-${\bf a}$ware ${\bf l}$ogical ${\bf f}$ramework for studying quantitative aspects of functional programs with effects. Like ${\bf 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 ${\bf calf}$, the present language takes account of effects, such as probabilistic choice and mutable state; this extension requires a reformulation of ${\bf 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 ${\bf 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 ${\bf decalf}$ via a model in the topos of augmented simplicial sets.

翻译：我们提出${\bf decalf}$，一种定向的、带效应的代价感知逻辑框架，用于研究含效应函数式程序的量化性质。与${\bf calf}$类似，该语言基于程序的外延与内涵之间的形式化阶段区分——即程序的纯行为与通过带效应的步数计数原语度量的代价之间的区别。类型理论确保行为不受代价计算的影响。与${\bf calf}$不同，本语言考虑了概率性选择与可变状态等效应；这一扩展需要对${\bf calf}$的代价计算方法进行重新表述：此处不再依赖"可分离"的代价概念，而是将代价界限视为另一个程序。为使其形式化，我们为每种类型配备一个内在预序，将程序内在的精确代价计算松弛为一种更宽松但仍具信息量的估计。例如，概率程序的代价界限本身就是一个指定代价分布的概率程序。该方法可作为标准方法的简化替代方案，标准方法通过提取递归关系来界定代价，而本方法可直接推广到高阶含效应程序。我们首先介绍${\bf decalf}$类型系统，该系统基于项之间的内在排序：在外延阶段，该排序限制为外延相等；而在内涵阶段，它反映目标程序代价的近似。随后，我们将这种形式化应用于多个示例，包括纯排序算法与含效应排序算法、简单概率程序以及高阶函数。最后，我们通过增广单纯集拓扑斯中的模型来论证${\bf decalf}$的合理性。