2016/12/04 by Annabelle McIver, McIver, Annabelle, Carroll Morgan +1 · 3 citations
Computer Science · #Logic, Reasoning, and Knowledge #Bayesian Modeling and Causal Inference #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1612.01091
Extending our own and others' earlier approaches to reasoning about\ntermination of probabilistic programs, we propose and prove a new rule for\ntermination with probability one, also known as "almost-certain termination".\nThe rule uses both (non-strict) super martingales and guarantees of progress,\ntogether, and it seems to cover significant cases that earlier methods do not.\nIn particular, it suffices for termination of the unbounded symmetric random\nwalk in both one- and two dimensions: for the first, we give a proof; for the\nsecond, we use a theorem of Foster to argue that a proof exists.\nNon-determinism (i.e. demonic choice) is supported; but we do currently\nrestrict to discrete distributions.\n