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.
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] ]
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 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:
The particular approach taken here has elements in common with Automath (in that we use a small core language including proof terms), Mizar (in that we use Tarski-Grothendieck set theory and are attempting to form a library of formalized mathematics), Isabelle (in that we use a form of simple type theory as a framework) and Coq (in that we largely use the syntax of Coq for types, terms and proofs).
This shows that at least an alternative goal of the site is to build a library of formalized mathematics. However, recent announcement reveals that Mathgate was also to be a gambling site of sorts, bringing revenue to the owner. The idea was that people would pay up-front for access to exercises in proving theorems. Then they would participate in a treasure hunt – if their proof is correct and corresponds in some way (I guess by comparing the proof term) to the proof the author had in mind, they would be awarded some bitcoins. That idea did not fly, as the author says
I will no longer advertise it because I have no more hope of making it into a self-sustaining business. Since I’ll have to find another way to support myself, mathgate.info will only be a hobby and won’t be as active as it could’ve otherwise been.
Apparently the number of COQ programmers interested in formalized mathematics and gambling is too small.
I have to say I got encouraged by the treasure hunt and spent some effort to learn the proof language used on Mathgate. That was a rather frustrating experience for many reasons. The relevant information is scattered all over the site. There are instructional videos, and they are good, but there there is no tutorial that would describe tactics with examples of their usage. There is a document with a one-sentence description of each tactic, but with no examples and I think it simply does not tell everything needed. The error messages from the prover are rather unhelpful (like “Failure: Not a tp”).
Freek Wiedijk once gave a nice description of declarative vs. procedural proof languages
A declarative system is one in which one writes a proof in the normal way, although in a highly stylized language and with very small steps. (…) In a procedural system one does not write proofs at all. Instead one holds a dialogue with the computer. In that dialogue the computer presents the user with proof obligations or goals, and the user then executes tactics, which reduce a goal to zero or more new, and hopefully simpler, subgoals.
As a result I kept getting stuck on trivialities. Typically in such cases one asks a question on some community forum, but there is no such thing for Mathgate. I really don’t remember having such hard time when I was learning the Isar proof language. Since the tactics supported by the Mathgate language are very similar to some COQ tactics I think the best way to learn the Mathgate proof language is to learn COQ first, and then use the experience.
After maybe 10 hours of watching videos, looking at provided example proofs and trial end error I finally was at the point when I was able to write some proofs that claimed to have milibitcoins associated with them. I did have some sense of accomplishment, even though I got “Your proof is correct but does not correspond to the declared treasure”.
I hope Dr. Chad E. Brown keeps working on Mathgate. The most important improvement would be to create a declarative language layer on top of the low – level tactics supported now – something like COQ’s C-zar. I am sure more people would be interested in formal proving if the experience was not so far removed from traditional mathematical practice.
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.
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.
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.
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, 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 knew that day would come at some point. I am programming in Java. One thing that took me longer that I think it should was to figure out how to use Mockito‘s ArgumentCaptor to verify arguments with which methods are called. In this post I share some code snippets that do that, for my reference and hopefully to help other Java beginners.