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

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