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

Interval arithmetic in groups – pass 2

This is a continuation of the Interval arithmetics in groups: Pass 1 post.

Let be a binary operation on a set . We will write this operation additively as . Such operation defines another binary operation on on the powerset (set of subsets) of in a natural way: for .  The nice thing about is that it inherits interesting properties of : if is commutative, then so is , if is a semigroup, then is also a semigroup, if is a monoid, then is also a monoid, if is a group. then … well, never mind, we don’t need that anyway.

This means that all theorems about adding finite (indexed) collections of semigroup elements (and there are quite a couple in the Semigroup_ZF theory) can be reused for the operation on subsets of at little additional cost.

The setup for adding group subsets in the Gyula Lakos’s paper is different in that it assumes the existence of neutral element and defines how to add an infinite number of subsets of .

b.) More generally, suppose is a countable indexed family of subsets of . Assume that for all except for finitely many. Only in that case we define the algebraic sum as except for finitely many .

We can do something in that spirit for as well. Namely suppose that
is a monoid and is a an indexed collection of subsets of such that all but finitely many contain the neutral element (denoted ). We can split the index set  into two subsets, one called consisting of those for which contains the neutral element, and the rest. Then we can define the sum of the family of subsets of as follows:

where is the set of finite nonempty subsets of and are interpreted as the additive notation for . So what we do is we add all sets that do not contain , but for sets that do contain we sum every finite subcollection and take the union of all sums obtained this way.

This nicely generalizes the concept of adding finite collections of sets of semigroups (where the is empty and there is only the first component of the sum above) and (in contrast to the Lakos’ approach) does not require selecting monoid elements from infinite collections of subsets of , i.e. does not require the axiom of choice.

IsarMathLib version 1.6.7 released

This release includes the new HTML rendering tool that replaces tiddlyisar (which still compiles and works ). I updated all IsarMathLib theories that were not fully updated for Isabelle 2008 removing legacy keywords like constdefs and prems and added missing comments. As a result all IsarMathLib theories except those translated from Metamath are now presented at the FormalMath.org site.

There is no new formalized mathematics in this release.

Goodbye ProofGeneral

Some recent messages on the Isabelle mailing list bring the information that the Isabelle team is working on a new interface for Isabelle and possibly other provers that will replace Emacs based ProofGeneral. The new interface will be written in Scala. Scala is an multiparadigm language (OO and functional) that runs on JVM. This is an interesting choice of technology that suggests something about the design goals (I am speculating again). Applications writen in Scala can run on any platform that has JVM. In particular, one can write applets in Scala that can be run in a browser. Scala is a general purpose language, but seems to be particularly good for web programming. There are a couple of web programming frameworks written in Scala, Lift being the most popular, competing with Rails. So the new interface will be multiplatform and easy to integrate with web applications (wiki?). Hopefully this will make Isabelle proving environment closer to being network transparent – a user interface, possibly running in a browser and sending formalized text for verification to an Isabelle server located (possibly) on a different host with dependencies scattered all over the internet.

Formalmath.org

The new HTML rendering of IsarMathLib is ready.

Creating it was easier than I had expected. The most tricky part of the Isar to HTML translator is the Isar parser, but that was done when creating the TiddlyWiki rendering, and didn’t require any changes. Producing HTML from internal representation was just a simple rewrite of the existing TiddlyWiki markup generator. I had to learn some JavaScript and haXe to implement expanding proofs and reference hints, but not much and it was an interesting experience.The CSS layout was created with an online frameset generator with some minor tweaks.

There is one remaining serious issue that I don’t know how to resolve. Some proofs don’t expand on click. One can see an example of this problem in the proof of lemma func1_1_L12 in the func1 theory. The only subproof there does not change cursor and background color on mouse hover (implemented with CSS) and does not expand on click (haXe and JavaScript). Curiously, TiddlyWiki presentation has a very similar problem, see the proof of prod_list_of_lists in the Semigroup_ZF tiddler. This happens in Firefox 3.0.5 on Ubuntu and IE7 and Firefox on Windows XP. If you have an idea what might be causing this, please let me know.

P.S. This turned out to be a jsMath issue.