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 immediately, each with probability $1/2$. For normal form programs, we provide a 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}$.

翻译：我们研究了带有有理变量、有界非确定性选择和离散概率选择的命令式编程语言中正几乎必然终止（$\mathsf{PAST}$）的递归论复杂性。若对于每个调度器，程序几乎必然终止且期望运行时间有限，则该程序满足正几乎必然终止。我们证明了该语言中的$\mathsf{PAST}$问题对于（光面）共解析集是完备的（$\Pi^1_1$-完备）。这与相关的几乎必然终止（$\mathsf{AST}$）和有界终止（$\mathsf{BAST}$）概念形成对比，后两者均为算术集（分别为$\Pi^0_2$和$\Sigma^0_2$完备）。我们的上界给出了一种有效方法，可将概率终止推理简化为有界非确定性模型中的非概率公平终止，以及无界非确定性模型中的简单程序终止。下界则揭示了相反方向：对于每个带无界非确定性选择的程序，存在一个有效可计算的有界选择概率程序，使得原程序终止当且仅当变换后程序是$\mathsf{PAST}$的。我们证明了每个程序都存在有效可计算的规范形式，其中每个概率选择以1/2的概率继续或立即终止执行。对于规范形式程序，我们给出了$\mathsf{PAST}$的可靠且完备的证明规则。该规则使用超限序数，并证明推理$\mathsf{PAST}$需要达到$\omega^{CK}_1$的超限序数；因此，基于将程序状态映射到实数的秩超鞅的现有概率终止技术不足以推理$\mathsf{PAST}$。