On the Hardness of Almost-Sure Termination

TL;DR

This paper investigates the computational complexity of determining almost-sure termination and expected outcomes in probabilistic programs, revealing high levels of logical hardness in these decision problems.

Contribution

It establishes the precise arithmetical hierarchy levels for the complexity of various almost-sure termination and expectation problems in probabilistic programs.

Findings

Lower and upper bounds of expected outcomes are $oldsymbol{ ext{Sigma}_1^0}$- and $oldsymbol{ ext{Sigma}_2^0}$-complete.

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

Deciding positive almost-sure termination is $oldsymbol{ ext{Sigma}_2^0}$-complete.

Abstract

This paper considers the computational hardness of computing expected outcomes and deciding (universal) (positive) almost-sure termination of probabilistic programs. It is shown that computing lower and upper bounds of expected outcomes is $\Sigma_1^0$- and $\Sigma_2^0$-complete, respectively. Deciding (universal) almost-sure termination as well as deciding whether the expected outcome of a program equals a given rational value is shown to be $\Pi^0_2$-complete. Finally, it is shown that deciding (universal) positive almost-sure termination is $\Sigma_2^0$-complete ($\Pi_3^0$-complete).