Decalf：一个定向的、有影响力的成本感知逻辑框架
摘要：$f decalf$：一种用于研究带有效果的功能性程序的定量方面的有向、具有效果的成本感知的逻辑框架。与$f calf$类似，该语言基于程序的扩展和内涵之间的正式阶段区分，即纯行为与通过效果步骤计数原语测量的成本行为。类型理论确保行为不受成本计算的影响。与$f calf$不同，目前的语言考虑到了效果，如概率选择和可变状态；这种扩展需要对$f calf$的成本计算方法进行重新规定：不再依赖可分离的成本概念，而是成本上界本身就是另一个程序。为了使此过程规范化，我们为每种类型都赋予了内在的预排序，将程序的精确成本计算松散地估计为另一个更加信息丰富但仍然宽松的预估。例如，概率程序的成本上界本身就是指定成本分布的概率程序。这种方法作为高阶、具有效果的程序中成本限制的标准方法的流畅替代。 首先，我们介绍了$f decalf$类型系统，它基于项之间的内在排序，在扩展阶段受限制于扩展相等性，但在内涵阶段则反映了程序成本的近似值。然后，我们将该公式应用于一些说明性示例，包括纯粹和具有效果的排序算法、简单的概率程序和高阶函数。最后，我们通过扩充单纯集的拓扑模型来证明$f decalf$。
作者：Harrison Grodin (1), Robert Harper (1), Yue Niu (1), Jonathan Sterling (2) ((1) Carnegie Mellon University, (2) Aarhus University)
论文ID：2307.05938
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-18