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

edit

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   is almost surely terminating on the input   if and only if

  [1][note 1]

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

Theoretical Complexity

edit

Positive Almost Sure Termination

edit

Probablistic Variants

edit

Notes

edit
  1. ^ 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

edit
  1. ^ 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.