On the Hardness of Almost-Sure Termination

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).}