Raising Expectations: Automating Expected Cost Analysis with Types
summary
A type-based tool called PRaML automatically infers upper bounds on expected execution cost for probabilistic OCaml-like programs by extending RaML’s AARA potential method and reducing inference to linear constraint solving. Soundness is proven against a new distribution-based operational semantics that handles divergence; expected-cost bounds imply almost-sure termination for step-count costs. Examples: a geometric recursion gets expected cost 2, gambler’s ruin yields A·B rounds, Von Neumann extraction gives 1/(p(1−p)) steps; most analyses run in under a second.
AI-written summary · about
chapters (9)
- 0:00Start
- 1:46AUTOMATED COST ANALYSIS
- 3:15POTENTIAL METHOD
- 4:11MEM
- 7:36FLIP RULE
- 10:07BERNOULLI
- 11:15PROBABILISTIC MODELS
- 12:55AVERAGE CASE ANALYSIS
- 14:04CONTRIBUTION
related talks
15mA Modular Cost Analysis for Probabilistic Programs
17mAutomated Expected Value Analysis of Recursive Programs
12mImplementing Hybrid Resource Analysis in Resource Aware ML
23mA Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
39mA Reusable Machine-Calculus for Automated Resource Analyses
20mSemantic foundations of potential-synthesis for expected amortised-cost analysis
22mProbabilistic Refinement Session Types
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…