Markov chains – simulation

I have to say it took me considerable effort to figure out how to use the part of Haskell’s probability library that deals with randomness and simulation. The intuition developed by programming in imperative languages is especially harmful here.

Haskell in Q

My new job will involve coding in Q. Q is a scripting language derived from APL. It is mostly used for stuff related to trading and finance. I don’t know it yet, I’m supposed to learn it on the job, so I decided to have a look at it.

Moving again

I have decided to move with my family to Poland. I will be describing the experience on another blog.

IsarMathLib version 1.6.9 released

I have released a new version of IsarMathLib. There are about 20 new theorems and a new theory on topological groups. The theory contains some basic definitions and notation and ends with a theorem that a subgroup of a topological group is a topological group.

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.

Probability monad

My favourite programming language Haskell has a nice library for doing calculations with probablility distributions, called probability.
The library was originally written by Martin Ewig and Steve Kollmansberger and then extended and packaged for convenient installation by Henning Thieleman. Its main idea for the implementation is to use the fact that “probability distributions form a monad” (from a paper by the authors of the library ). This post aims at translating this claim into standard probability notation and showing how it is used in the library.

IsarMathLib version 1.6.8 released

This release is  the first version of the IsarMathLib library for the new Isabelle2009. There is a little bit of new formalized mathematics as well.

Isabelle 2009 released

The Isabelle team has released version 2009. Updating IsarMathLib to Isabelle 2009 was very easy. I only had to make a couple of corrections to proofs that used assumptions implicitly. The only more complicated change was related to renaming variables in the locale syntax.

MathWiki project is hiring

Apparently the formalized mathematics project at Radboud University Nijmegen (NL) that I wrote about previously did get some funding after all and they are hiring two people to work on it. The PhD position is for 4 years and the postdoc position is 3 years. I hope that a usable formalized mathematics wiki will be available earlier.

The postdoc position pays a “maximum salary”  of 3755 Euro per month. Such wording immediately makes me curious what is the minimum … .