提高期望：使用类型自动化预期成本分析
Raising Expectations: Automating Expected Cost Analysis with Types
摘要：
本文提出了一种基于类型的分析，推导概率程序的预期执行成本的上限。分析是自然组成的，在成本模型中是参数化的，并且支持高阶函数和归纳数据类型。导出的边界是多元多项式，其是数据结构的函数。通过将类型推断简化为线性约束求解的局部类型规则来启用绑定推理。该类型系统基于潜在的摊还分析方法，并扩展了确定性程序的自动摊销资源分析（AARA）。一个主要的创新是边界可以包含符号概率，它可能出现在数据结构和函数参数中。另一个贡献是一个新的健全性证明，建立了正确性的衍生边界相对于一个基于分布的运营成本语义，也包括非平凡的发散行为。对于像时间这样的成本模型，导出的边界意味着以概率1终止。为了突出新颖的想法，演示文稿侧重于线性潜力和核心语言。然而，该分析被实现为资源感知ML的扩展，并且支持多项式边界和用户定义的数据结构。该技术的有效性进行评估，通过分析离散分布的样本复杂性，并与一种新的平均情况下估计的确定性方案，结合预期成本分析与统计方法。
英文摘要：
This article presents a type-based analysis for deriving upper bounds on the expected execution cost of probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher order functions and inductive data types. The derived bounds are multivariate polynomials that are functions of data structures. Bound inference is enabled by local type rules that reduce type inference to linear constraint solving. The type system is based on the potential method of amortized analysis and extends automatic amortized resource analysis (AARA) for deterministic programs. A main innovation is that bounds can contain symbolic probabilities, which may appear in data structures and function arguments. Another contribution is a novel soundness proof that establishes the correctness of the derived bounds with respect to a distribution-based operational cost semantics that also includes nontrivial diverging behavior. For cost models like time, derived bounds imply termination with probability one. To highlight the novel ideas, the presentation focuses on linear potential and a core language. However, the analysis is implemented as an extension of Resource Aware ML and supports polynomial bounds and user defined data structures. The effectiveness of the technique is evaluated by analyzing the sample complexity of discrete distributions and with a novel average-case estimation for deterministic programs that combines expected cost analysis with statistical methods.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
