FOM discussion

October 25, 2014

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 $x:\mathbb{N}\rightarrow\mathbb{R}$ that is increasing and bounded and for any $y\in \mathbb{R}$ define $f(y) = x_{x^-1(y)+1}$ if $y\in x(\mathbb{N})$ and, say $f(y) = y+1$ otherwise. Then we have $x_{n+1} = f(x_n)$ and $f(y)>y$ for all $y\in\mathbb{R}$, but we have chosen the sequence $x$ 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 $f$ 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

October 20, 2014

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

September 19, 2014

In set theory there is a convenient notation for defining new sets, called set comprehension. For example when we have a set $A$ we can define a collection of singleton sets with elements from the set  $A$ as $\{ \{x\}:x\in A\}$. Sometimes vertical bar is used instead of the colon, and in Isabelle/ZF a single dot is used (something like $\{ \{x\}. x\in A\}$ 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

July 30, 2014

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:

KDB+, Elm and web sockets

July 15, 2014

In the KDB+ implementation of the Conway’s Game of Life that I presented in my previous post there was one element missing – a GUI that would display the results of the simulation. Since I have been planning to have a look at Elm for a while, I checked if I can set up KDB+ talking to an Elm application and it turned out it is very easy to do – with web sockets.

Elm is a functional programming language that compiles to HTML, JavaScript and CSS code intended to run in a browser. The declared paradigm for Elm is Functional Reactive Programming. FRP is not exactly what it used to be back in the days of Conal Elliot and Paul Hudak’s original work. It is now more of a buzzword covering more and more semantic area. The key concept in the  Elm’s take on FRP are signals. A Signal a type in Elm represents a value of type a that changes in time. Signals can be thought of as streams of discrete events carrying values. They can be combined, filtered, counted and so on. Ultimately we obtain a value of type Signal Element that can be displayed in the browser (possibly in a div if one embeds an Elm application this way). The Elm site contains a very convincing argument on why all this is a good idea.

Game of Life with Enterprise Components

May 20, 2014

DEVnet (the company I work for) has decided to release one of its products – Enterprise Components (called EC below) – as free software. Since I contributed some code to it I would like to advertise it a bit on this blog.

What are Enterprise Components?

EC is a collection of libraries and tools that support building systems based on KDB+ – a database made by Kx Systems. Traditionally KDB+ has been mostly used for time series analytics in finance industry. Part of the reason for that was that the commercial license for KDB+ was very expensive. However, some two months ago Kx announced that they now allow commercial use of the free-of-cost 32-bit version of their product. This opened a path for KDB+ applications in areas well beyond institutions with deep pockets.

The main limitation of the 32-bit version is the amount of data it can handle – about 1GB. This limitation is per-process though and since KDB+ has a built-in inter-process communication protocol one can create very capable systems using the free version just running as many instances as needed.

Enterprise Components can be thought of as a layer above KDB+. EC provide logging, process management, configuration management, user access control, system monitoring and more – all that is needed if you want to build a larger scale system. Typical use cases are covered in the standard components provided with EC so that one can define a basic system with data feeds, in-memory database backed by on-disk journals and storage and archiving at the end of day with configuration only.

ProofPeer

February 1, 2014

ProofPeer is a project to create a cloud-based social network interactive theorem proving system. I wrote about it a year ago. The project looked dormant since about July, but now it got funding and is accepting PhD studentship applications.

Proof market

January 11, 2014

Yoichi Hirai has created a site where one can submit bounties for proofs of theorems in Coq formal proof management system.  Currently the bounties are sent to a Bitcoin address that is under the control of the site owner. This requires of course  some trust in the site owner, although reducing the trust requirements is under discussion. I don’t think it is possible to implement a Coq checker in Script though (as Yoichi suggests) as Script is not Turing complete. Something like what is described in the Using external state chapter of the Bitcoin wiki page on contracts is more realistic.

There are currently bounties for proving False (i.e showing inconsistency of Coq) and a couple of theorems that seem quite involved. The funny thing is proving False is also on the list of solved problems. Someone has earned 0.999 BTC by submitting four lines that just change the meaning of False and state a trivial theorem using that changed meaning, thus showing Pollack-inconsistency of Coq.

Bitcoin epic fails

January 4, 2014

Bitcoin, or more generally cryptocurrencies  is  a somewhat complex subject in that it connects technology, economics and law. But it is kind of fashionable now, so some famous people decide to publicly formulate opinions about it without devoting time and effort to gain knowledge about how the technology actually works. As one commenter on the Marginal Revolution site nicely put it:

The situation has all the makings of your standard paradigm shift, where pundits with less neurological plasticity give future history books lots of look-how-wrong-they-were quotes.
I would like to mention two examples of such epic fails.

IsarMathLib version 1.9.1 released

January 3, 2014

This is a maintenance release mostly to update IsarMathLib to Isabelle 2013-2. The RIPEMD-160 hash (a2ef972973bb2d072c7702d28dcfabee9026bd3b) of the proof document for this release is timestamped in the Bitcoin blockchain at 1FrXV7eifF2zruVr8YHJdvV8GHucUAqxYy.