一句话：提出 pλ-amor，用分级模态类型论证明高阶概率程序的期望代价界。
在线学习算法通常需要优化并证明其产生的损失或代价界，但这些算法依赖随机性，损失函数常定义为期望，精确界常为非多项式（如对数级），最优性证明常依赖势函数论证。本文提出 pλ-amor，一个针对带递归的高阶概率程序进行期望代价分析的效应式分级模态类型论框架。它扩展了确定性程序代价分析工作 λ-amor，用分级模态类型在类型层面表示势、代价与概率。作者通过一个 Kripke 步进索引模型证明 pλ-amor 的可靠性，该模型将势与概率耦合联系起来，并用该框架证明了在线机器学习文献中若干例子的代价界。最后，文中给出 pλ-amor 在分级余单子下的扩展，并讨论不同模态之间的关系。
The design of online learning algorithms typically aims to optimise the incurred loss or cost , e.g., the number of classification mistakes made by the algorithm. The goal of this paper is to build a type-theoretic framework to prove that a certain algorithm achieves its stated bound on the cost. Online learning algorithms often rely on randomness, their loss functions are often defined as expectations, precise bounds are often non-polynomial (e.g., logarithmic) and proofs of optimality often rely on potentialbased arguments. Accordingly, we present pλ-amor, a type-theoretic graded modal framework for analysing (expected) costs of higher-order probabilistic programs with recursion. pλ-amor is an effect-based framework which uses graded modal types to represent potentials, cost and probability at the type level. It extends prior work ( λ-amor) on cost analysis for deterministic programs. We prove pλ-amor sound relative to a Kripke step-indexed model which relates potentials with probabilistic coupling. We use pλ-amor to prove cost bounds of several examples from the online machine learning literature. Finally, we describe an extension of pλ-amor with a graded comonad and describe the relationship between the different modalities.
@article{RajaniB024,
title = {A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs},
author = {Vineet Rajani and Gilles Barthe and Deepak Garg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689725}
}