Raising Expectations: Automating Expected Cost Analysis with Types

TL;DR

This paper introduces a type-based analysis method for automatically deriving upper bounds on the expected cost of probabilistic programs, supporting complex data structures and higher-order functions, with applications in average-case analysis.

Contribution

It extends automatic amortized resource analysis to probabilistic programs with symbolic probabilities, providing a sound, compositional framework for cost bounds.

Findings

Successfully derives polynomial bounds for probabilistic programs.

Supports symbolic probabilities in data structures and functions.

Evaluates effectiveness through sample complexity and average-case estimation.

Abstract

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.