Positive Almost-Sure Termination: Complexity and Proof Rules

Explore the complexity and proof rules of Positive Almost-Sure Termination (PAST) in this 19-minute conference talk from ACM SIGPLAN's POPL'24. Delve into the recursion-theoretic complexity of PAST in an imperative programming language featuring rational variables, bounded nondeterministic choice, and discrete probabilistic choice. Discover how PAST is complete for co-analytic sets ($\Pi_1^1$-complete), contrasting with Almost-Sure Termination (AST) and Bounded Termination (BAST). Learn about the effective procedure to reduce probabilistic termination reasoning to non-probabilistic fair termination or program termination in different models. Examine the transformation of programs with unbounded nondeterministic choice to probabilistic programs with bounded choice. Understand the concept of normal form for programs and its significance in PAST analysis. Explore the first sound and complete proof rule for PAST, which utilizes transfinite ordinals up to $\omega^{CK}_1$, and grasp why existing techniques based on ranking supermartingales are insufficient for PAST reasoning.