Formalpedia

Formalpedia is an “editable online repository of code and formal math”. It is on its way to became the first formalized mathematics wiki that goes online.

Markov chains

The approach taken in the Haskell’s probability library makes it especially convenient for modeling Markov chains.
Suppose  is a Markov chain on a state space . Distribution of the process is determined by the distribution of and the numbers , , called transition probabilities. For simplicity let’s consider only time-homogeneous Markov chains where these numbers don’t depend on and let’s assume that the initial distribution is a point mass, i.e. for some . Then we can define a function , where for each the value is a distribution on defined by . Here denotes the set of finitely supported nonnegative functions on that sum up to 1. Conceptually, is the the distribution of the next value of the chain given the current value is . This is exactly the kind of distribution-valued function that is the right hand side operand of the operation from the previous post, which corresponds to the Haskell’s >>= operation in the probability monad.