Analyzing Expected Outcomes and Almost-Sure Termination of Probabilistic Programs is Hard

TL;DR

This paper investigates the computational complexity of analyzing probabilistic programs, showing that key problems like almost-sure termination and expected outcome equivalence are highly undecidable, with varying degrees of computational hardness.

Contribution

It establishes the precise computational hardness of deciding almost-sure termination and expected outcomes, providing a detailed complexity classification for these problems.

Findings

Deciding almost-sure termination is $ ext{Pi}^0_2$-complete.

Deciding whether the expected outcome equals a given rational value is $ ext{Pi}^0_2$-complete.

Bounding expected outcomes is recursively enumerable and $ ext{Sigma}^0_2$-complete.

Abstract

This paper considers the computational hardness of computing expected outcomes and deciding almost-sure termination of probabilistic programs. We show that deciding almost-sure termination and deciding whether the expected outcome of a program equals a given rational value is $\Pi^0_2$-complete. Computing lower and upper bounds on the expected outcome is shown to be recursively enumerable and $\Sigma^0_2$-complete, respectively.