User:PhoenixIra/Almost Sure Termination

A probablistic program is called almost surely termninating, if on every input the probablitiy the program terminates is 1.^[1] In other words, it is probabilistic guaranteed to terminate. This does not mean that the program does not allow non-terminating paths, but hese have a probability mass of 0. This also does not mean that the program terminates in a reasonable time, as the program could have an expected runtime of infinity.

Definition

A program is almost surely terminating, if the input is terminating with probablitiy 1 on one or all inputs. If it is only terminating with probability 1 on a specific input, the input is usually explicitly stated. Formally, we say a program $P$ is almost surely terminating on the input $\sigma$ if and only if

  $\mathbb {P} (P(\sigma ){\text{ terminates}})=1.$ ^[1]^{[note 1]}

We say a program $P$ is almost surely terminating if and only if $P$ almost surely terminats on all inputs.

Theoretical Complexity

Positive Almost Sure Termination

Probablistic Variants

Notes

^ This is usually defined by means of the semantics. However, introducing a formal semantics for probabilistic programs is out of scope for this article.

Rerefrences

^ ^a ^b McIver, Annabelle; Morgan, Carroll; Kaminski, Benjamin Lucien; Katoen, Joost-Pieter (December 2017). "A new proof rule for almost-sure termination". Proceedings of the ACM on Programming Languages. 2 (POPL): 33:1-33:43. doi:10.1145/3158121.

[2] This is usually defined by means of the semantics. However, introducing a formal semantics for probabilistic programs is out of scope for this article.

[AST-proof-rule-1] McIver, Annabelle; Morgan, Carroll; Kaminski, Benjamin Lucien; Katoen, Joost-Pieter (December 2017). "A new proof rule for almost-sure termination". Proceedings of the ACM on Programming Languages. 2 (POPL): 33:1-33:43. doi:10.1145/3158121.

[1]

[note 1]