Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Denotational Foundations for Expected Cost Analysis

Pedro H. Azevedo de Amorim

TL;DR

The paper introduces $\mathbf{cert}$, a CBPV-based metalanguage for probabilistic cost analysis, addressing the non-deterministic nature of cost due to sampling.It develops two denotational semantics: a cost semantics via a writer monad transformer and an expected-cost semantics as a monad on $[0,\infty] \times P_{\le 1}$ over $\omega$-quasi-Borel spaces, with proven soundness and adequacy.A generalized effect-simulation property and a canonicity theorem show that the expected-cost monad is the minimal cost-aware submonad of the continuation monad $K_{[0,\infty]}$, providing a robust semantic framework.Case studies, including randomized quicksort and stochastic convex hull, demonstrate compositional reasoning about the expected cost of non-trivial probabilistic algorithms.

Abstract

Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the probabilistic samples made throughout the execution of the program. This interaction is further complicated by the non-trivial interaction between cost, recursion and evaluation strategy. In this work we introduce $\mathbf{cert}$: a Call-By-Push-Value (CBPV) metalanguage for reasoning about probabilistic cost. We equip $\mathbf{cert}$ with an operational cost semantics and define two denotational semantics -- a cost semantics and an expected-cost semantics. We prove operational soundness and adequacy for the denotational cost semantics and a cost adequacy theorem for the expected-cost semantics. We formally relate both denotational semantics by stating and proving a novel \emph{effect simulation} property for CBPV. We also prove a canonicity property of the expected-cost semantics as the minimal semantics for expected cost and probability by building on recent advances on monadic probabilistic semantics. Finally, we illustrate the expressivity of $\mathbf{cert}$ and the expected-cost semantics by presenting case-studies ranging from randomized algorithms to stochastic processes and show how our semantics capture their intended expected cost.

Denotational Foundations for Expected Cost Analysis

TL;DR

The paper introduces $\mathbf{cert}$, a CBPV-based metalanguage for probabilistic cost analysis, addressing the non-deterministic nature of cost due to sampling.It develops two denotational semantics: a cost semantics via a writer monad transformer and an expected-cost semantics as a monad on $[0,\infty] \times P_{\le 1}$ over $\omega$-quasi-Borel spaces, with proven soundness and adequacy.A generalized effect-simulation property and a canonicity theorem show that the expected-cost monad is the minimal cost-aware submonad of the continuation monad $K_{[0,\infty]}$, providing a robust semantic framework.Case studies, including randomized quicksort and stochastic convex hull, demonstrate compositional reasoning about the expected cost of non-trivial probabilistic algorithms.

Abstract

Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the probabilistic samples made throughout the execution of the program. This interaction is further complicated by the non-trivial interaction between cost, recursion and evaluation strategy. In this work we introduce : a Call-By-Push-Value (CBPV) metalanguage for reasoning about probabilistic cost. We equip with an operational cost semantics and define two denotational semantics -- a cost semantics and an expected-cost semantics. We prove operational soundness and adequacy for the denotational cost semantics and a cost adequacy theorem for the expected-cost semantics. We formally relate both denotational semantics by stating and proving a novel \emph{effect simulation} property for CBPV. We also prove a canonicity property of the expected-cost semantics as the minimal semantics for expected cost and probability by building on recent advances on monadic probabilistic semantics. Finally, we illustrate the expressivity of and the expected-cost semantics by presenting case-studies ranging from randomized algorithms to stochastic processes and show how our semantics capture their intended expected cost.
Paper Structure (49 sections, 52 theorems, 49 equations, 13 figures)

This paper contains 49 sections, 52 theorems, 49 equations, 13 figures.

Table of Contents

  1. Introduction
  2. Our Work: Denotational Methods for Expected Cost
  3. Our contributions
  4. $\mathbf{cert}$ : A Probabilistic Cost-Aware Metalanguage
  5. Cost and Probabilistic Effects
  6. Lists
  7. Equational Theory
  8. Operational Semantics
  9. Syntax Spaces and Kernels
  10. Operational Kernels
  11. Denotational Semantics
  12. $\omega$-quasi Borel spaces
  13. Inductive types
  14. Probability Monads
  15. A probabilistic cost semantics
  16. ...and 34 more sections

Key Result

Lemma 2.8

If $\Gamma, x : \tau \vdash_c t : \overline{\tau}$ and $\Gamma \vdash_v V : \tau$ then $\Gamma \vdash_c t\{V / x\} : \overline \tau$.

Figures (13)

  • Figure 1: Types and Terms of CBPV
  • Figure 2: CBPV typing rules
  • Figure 3: Length function $\mathsf{length}$ (left) and filter function $\mathsf{biFilter}$ (right).
  • Figure 4: Equational Theory (Selected Rules)
  • Figure 5: Big-Step Operational Semantics
  • ...and 8 more figures

Theorems & Definitions (116)

  • Example 2.1: Geometric distribution
  • Example 2.2: Deterministic Programs
  • Example 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Lemma 2.8
  • Lemma 2.9: cf. Lemma 3.7 of Ehrhard et al. ehrhard2017
  • Lemma 2.10: Subject reduction
  • ...and 106 more