Positive Almost-Sure Termination – Complexity and Proof Rules
summary
Shows that Positive Almost-Sure Termination (PAST) for an imperative language with rational variables, bounded nondeterministic choice and discrete probabilistic choice is Π1^1-complete, using a reduction from recursive well‑founded ω‑trees and a transformation from unbounded nondeterminism to bounded probabilistic choice. Provides an effective normal (canal) form transform that preserves PAST, and a sound-and-complete proof rule uses transfinite ordinals (ranks up to ω1^CK) — demonstrates ranking supermartingales to reals are insufficient, and the constructions and reductions are effective and implementable.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:14Definition and motivation
- 3:01PAST vs BAST example
- 5:12PAST complexity Π₁¹-complete
- 9:30Reduction to PAST
- 11:14Canal form programs
- 13:45Ranking functions with ordinals
- 14:49Proof rule soundness
- 15:09Summary of results
- 15:32Q&A
related talks
24mIntersection Types and (Positive) Almost-Sure Termination
43mControlling Probabilistic Systems Under Partial Observation
01h 00mLogic and Probabilistic Circuits 3
49mSemantic Foundations for Probabilistic Programming
20mStatic Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
24mHigher order programming with probabilistic effects: A model of stochastic memo...
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
01h 00mKeynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic(…)