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. Read the rest of this entry »
Formalpedia
June 15, 2009 by slawekkMarkov chains
June 5, 2009 by slawekkThe 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. Read the rest of this entry »
Probability monad
May 31, 2009 by slawekkMy 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. Read the rest of this entry »
IsarMathLib version 1.6.8 released
April 26, 2009 by slawekkThis release is the first version of the IsarMathLib library for the new Isabelle2009. There is a little bit of new formalized mathematics as well. Read the rest of this entry »
Isabelle 2009 released
April 22, 2009 by slawekkThe 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. Read the rest of this entry »
MathWiki project is hiring
March 10, 2009 by slawekkApparently 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
March 1, 2009 by slawekkThis 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
February 18, 2009 by slawekkThis 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
January 15, 2009 by slawekkSome 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
January 7, 2009 by slawekkThe 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.