Jump to content

User:PhoenixIra/Almost Sure Termination

From Wikipedia, the free encyclopedia

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.