IsarMathLib updated to Isabelle2016-1

I finally got around to update IsarMathLib to Isabelle2016-1 that was released in  December last year. This was a quite time consuming update. The Isabelle system integrates LaTeX to be able to typeset well looking document proofs. This indeed works well – when it does. When there is a problem though it requires  LaTeX specific knowledge or long time to fix. This is what happened this time. The Isabelle team removed an element of its LaTeX setup that was obsoleted a couple of releases ago. They provided a script that was supposed to make necessary changes to theory files, but in my case running it on IsarMathLib’s 78 theory files just caused the errors to multiply. Fortunately Isabelle distribution sources provide lots of examples how LaTeX should be currently set up. After struggling for some time to understand the errors scattered over a 10MB log file I just created the IsarMathLib LaTeX setup from scratch following the examples and it worked. The IsarMathLib’s proof document and outline look better than ever.

Advertisements

Visualizing Pandas GroupBy object

I am a beginner again, this time learning Python and Pandas. I am enjoying it quite a lot. For learning I write code in a Jupyter notebook and this post is actually written as one – converted to HTML with nbconvert. The quality of the conversion is rather bad, but this is probably the best one can do without adding custom CSS to this blog setup, which would require upgrading to WordPress.com Premium.

Development using Jupyter  is similar to how KDB+ coding is mostly done. In KDB+ one sends commands to a KDB+ server from a client like Studio for KDB+, getting an instant feedback on the result. Pandas is not as expressive and concise as q, but the style of a high-level API for vectorized data manipulation with avoidance of explicit iteration (loops) is similar.

One exception to the instant feedback rule in Jupyter and Pandas is the GroupBy object. To see what I mean let’s define a simple data frame from a dictionary of columns:

In [1]:

import pandas as pd
data = pd.DataFrame({'sym':['a','b','c'],
                     'price1':[100.0,150.0,130.0],
                     'price2':[110.0,150.0,120.0],
                     'vol1':[1000.0,1200.0,1300.0],
                     'vol2':[1500.0,1300.0,1100.0]})
data

Out[1]:

	price1	price2	sym	vol1	vol2
0	100.0	110.0	a	1000.0	1500.0
1	150.0	150.0	b	1200.0	1300.0
2	130.0	120.0	c	1300.0	1100.0

Grouping is more often done for rows (along the 0 axis), but this time we want to group columns (along axis=1). One group is made of the price1 and price2 columns, the second one groups vol1 and vol2 and the sym column forms its one element group. To do this we define a function that takes a column name and classifies it into one of three categories:

In [2]:

def classifier(column):
    if column.startswith('price'): return 'price'
    if column.startswith('vol'): return 'volume'
    return 'sym'

Now we can group the columns using the classifier:

In [3]:

data.groupby(classifier,axis=1)

Out[3]:

<pandas.core.groupby.DataFrameGroupBy object at 0x00000048DE8A1CF8>

As we can see, the GroupBy object is not printed nicely (at least in Pandas 0.19.2 that I am using).
Of course, there are many ways to print it. One way that I found intuitive and useful is to first convert the GroupBy object to a dictionary of dataframes keyed by the classifier value. This can be done using the dictionary comprehension like {grp:subdf for grp,subdf in df.groupby(classifier,axis=1)}. The dictionary obtained this way can be passed to Panda’s concat function. concat puts the dictionary of dataframes together to get a single dataframe with multi-level columns. The additional column level clearly shows the structure of the original GroupBy object.

In [4]:

def groupCols(df,classifier):
    return pd.concat({grp:subdf for grp,subdf in df.groupby(classifier,axis=1)},
                     axis=1)

groupCols(data,classifier)

Out[4]:

	price		sym	volume
	price1	price2	sym	vol1	vol2
0	100.0	110.0	a	1000.0	1500.0
1	150.0	150.0	b	1200.0	1300.0
2	130.0	120.0	c	1300.0	1100.0

This trick also works for classifying rows if one uses axis=0 instead of axis=1 in a function similar to groupCols above.

Cheap air quality monitoring

About a year ago I set up an air quality monitoring station based on the Air Quality Egg product by Wicked Device (see also my previous post on AQE). It was working during the winter season, providing real time data on PM2.5 concentrations near my house. This graph shows some of the data collected.

This worked OK, except that the data from the device were uploaded to Xively and available only from there. Xively was providing this service free as it was fulfilling an old commitment from one of their acquisitions. It was not high on their priority list and the service was frequently down. I decided to build my own device then to have full control over the process – from collecting the data to displaying them on a public web page. And to have some creative fun. The result works well (at least at the time of the writing) and cost less than $80 in materials, including a Raspberry Pi that I used. I think building a PM2.5 monitoring station in a way similar to what I describe below would make an excellent high school project.

IsarMathLib 1.9.4 and other news

I updated IsarMathLib to work with Isabelle 2016 a couple of weeks ago. The distribution and the proof document are available in the usual places.

In other news, back in October 2015 Daniel De La Concepción, an IsarMathLib contributor, published an informal version of some of his contributions in a paper titled “New equivalences to axioms weaker than AC in topology”.

 

IsarMathLib 1.9.3 released

This is a maintenance release to update IsarMathLib for Isabelle2015. There is no new formalized mathematics in this release.

Air Quality Egg

Air quality in Poland is in general rather poor, according to some sources the second worst in Europe. I live in Poland in a small town of about 9000 people. Since it is close to Wrocław, people consider it rural. There is some truth in that – it is surrounded by forests that are a great place to walk or bike. As far as air pollution is concerned however, the situation is bad, in winter worse than in Wrocław in my opinion. One evening last December after I came back from a walk smelling like a life-long chain smoker I tried to find data to check what is the level of pollution in my town. It turned out that probably nobody knows as almost all air quality monitoring in Poland concentrates in big cities. There are three monitoring stations in Wrocław, but none in the surrounding areas. So then I searched for an inexpensive way to measure pollution by myself and I found Air Quality Egg.

FOM discussion

There is a very interesting discussion about formalized mathematics going on the Foundations of Mathematics mailing list. The most interesting part of it (at least to me) is the thread about relative merits of Homotopy Type Theory (HoTT) and set theory (ZFC) as foundations for formalized mathematics. I should probably write what is Homotopy Type Theory here, but since I know very little about it this is too much risk to say something stupid, so I suggest that interested readers have a look at the above link, or read at least the abstract of the recent article about this in the Bulletin of the American Mathematical Society. Replacing ZFC with HoTT as standard foundation for mathematics is an idea of Vladimir Voevodsky – a Fields Medalist from 2002. The main argument for the idea is that it is easier to create research level formalized mathematics (in a proof assistant) when the foundation is HoTT than when foundation is set theory.  So the story is interesting from this perspective – that a prominent mathematician is using a proof assistant (COQ) for research and that ease of formalization is an argument for some mathematical idea – for the first time, to my knowledge.

I am not really convinced by the discussion on FOM that HoTT is “better” than ZFC in any universal sense. To me it looks rather that HoTT approaches the body of mathematics from a different side, figuratively speaking. This puts certain areas with active research (some subjects in algebraic topology) closer to foundations and therefore makes them easier to formalize, but at the cost other areas being put farther away. It is not obvious that this trade off is worth abandoning the whole traditional style of doing (even informal) mathematics which is very set theory oriented.

There have been some quite amusing moments in the discussion. One participant, rather sceptical to formalized mathematics posed the following question:

Here is a very simple statement which I often give to students as a first exercise in iteration, and to practice formal mathematics.

***
Let f be a real-valued function on the real line, such that f(x)>x for all x.
Let x_0 be a real number, and define the sequence (x_n) recursively by x_{n+1} := f(x_n). Then x_n diverges to infinity.
***

(…)
What effort would be required to formalize this kind of statement using current technology?

The funny thing here is that the statement is false. To see this, just take any sequence that is increasing and bounded and for any define if and, say otherwise. Then we have and for all , but we have chosen the sequence to be bounded…

This was used by some to point out usefulness of checking proofs by a machine, which would catch a mistake like this. Freek Wiedijk was polite enough to add the missing assumption about continuity of and provided a HOL Light verification script for a similar (but true) theorem. That didn’t work too well: Harvey Frieman called that script a “totally unacceptable ugly piece of disgusting garbage”. I think that was a bit too harsh – the second version written using Freek’s declarative miz3 language for HOL Light didn’t look that bad.

Isabelle/ZF on which IsarMathLib is based was mentioned in the discussion once – but only to say that it “hardly has any users”. Well, that was better than calling me “nobody” (as in “nobody uses it”) that I have seen before.

IsarMathLib 1.9.2 released

I have released a new version of IsarMathLib – a library of formalized mathematics for the ZF logic of the Isabelle theorem proving environment. This is a maintenance release mostly to fix a couple of proofs that were not checking with Isabelle 2014 released at the end of August. The project distribution can be downloaded from the GNU Savannah server and the Isabelle generated proof document provides information on all theorems formalized by the project. The outline document is a shorter version of that without proofs.

Binary comprehensions in Erlang

In set theory there is a convenient notation for defining new sets, called set comprehension. For example when we have a set we can define a collection of singleton sets with elements from the set  as . Sometimes vertical bar is used instead of the colon, and in Isabelle/ZF a single dot is used (something like parses successfully in Isabelle/ZF). In some programming languages a similar notation is used for lists. For example in Python one can write

[ [x] for x in [1,2,3] ]

to get a list of singleton lists and in Haskell

[ [x] | x <- [1,2,3] ]

gives the same.

Erlang also has a syntax for list comprehension, very similar to Haskell’s:

[ [X] || X <- [1,2,3] ]

The part X <- [1,2,3] above is called the generator expression.

Erlang has also something unique (as far as I know): binary comprehensions. This is a concept similar to the list comprehensions, but the dummy variable bound by the notation (x in the examples above) can range over binaries rather than lists. I found this very convenient when I was implementing Erlang interface to the  KDB+ IPC protocol.

Mathgate

Mathgate declares its purpose as a “website for learning logic and mathematics through formal proofs”. The author and owner of Mathgate is Chad E. Brown, who is also the author of Satallax – an automated theorem prover which has won a a couple of times on the CADE ATP Systems Competition. Mathgate is powered by a different prover, however, which is described as follows: