Positive Almost-Sure Termination -- Complexity and Proof Rules

We study the recursion-theoretic complexity of Positive Almost-Sure Termination ($\mathsf{PAST}$) in an imperative programming language with rational variables, bounded nondeterministic choice, and discrete probabilistic choice. A program terminates positive almost-surely if, for every scheduler, the program terminates almost-surely and the expected runtime to termination is finite. We show that $\mathsf{PAST}$ for our language is complete for the (lightface) co-analytic sets ($\Pi^1_1$-complete) - this is in contrast to the related notions of Almost-Sure Termination ($\mathsf{AST}$) and Bounded Termination ($\mathsf{BAST}$), both of which are arithmetical ($\Pi^0_2$ and $\Sigma^0_2$ complete respectively). Our upper bound implies an effective procedure to reduce reasoning about probabilistic termination to non-probabilistic fair termination in a model with bounded nondeterminism, and to simple program termination in models with unbounded nondeterminism. Our lower bound shows the opposite: for every program with unbounded nondeterministic choice, there is an effectively computable probabilistic program with bounded choice such that the original program is terminating $iff$ the transformed program is $\mathsf{PAST}$. We show that every program has an effectively computable normal form, in which each probabilistic choice either continues or terminates execution. For normal form programs, we provide the first sound and complete proof rule for $\mathsf{PAST}$. Our proof rule uses transfinite ordinals. We show that reasoning about $\mathsf{PAST}$ requires transfinite ordinals up to $\omega^{CK}_1$; thus, existing techniques for probabilistic termination based on ranking supermartingales that map program states to reals do not suffice to reason about $\mathsf{PAST}$.