Isabelle 2009-1 and IsarMathLib

The Isabelle team has just released Isabelle 2009-1. The latest release 1.6.9 of IsarMathLib checks out without any modification, so there is no update needed.

The new installation instructions on the Isabelle web site and the bundle file that can be downloaded from there are specific for Isabelle/HOL. To install Isabelle/ZF for IsarMathLib on x86 Linux one needs to download Isabelle2009-1.tar.gz, polyml-5.3.0.tar.gz,  ProofGeneral-3.7.1.1.tar.gz and ZF_x86-linux.tar.gz and do tar -C /usr/local -xzf on each of them. The installation can be finished by running

./bin/isabelle install -p /usr/local/bin

from /usr/local/Isabelle2009-1.UncategorizedUncategorized

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 become 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.