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.

Elm is an actively developed and young language – the development started in 2011. The Elm code that I quote below does not compile with the latest compiler release (0.12.3) as of time of this writing due to a bug in the WebSocket library that I stumbled upon. I tested the code with a development snapshot of the Elm compiler straight from GitHub after the bug was fixed, so it should work fine with the next compiler release.
So let’s talk about the code. What I want is to have the browser connect to the life.admin component (that collects the information about the state of the grid cells) and display the results of the simulation as a grid of white or black squares. Using web sockets is very simple both on the q side and the Elm side. In order to allow the browser to connect to the q process one needs to overwrite the built in .z.ws function. I do it as follows:

.admin.wsh:0;
/ overwrite z.ws
.z.ws:{
  .log.info[`admin] "web socket connection, command ",.Q.s1 x;
  .admin.wsh:neg .z.w;
  .admin.wsh .admin.bToString (.admin.gridi;.admin.gridj)#1b;
  };

The .z.ws function runs when a client connects to the KDB+ web socket interface. When .z.ws runs the variable .z.w is available containing the handle that we can use to send strings to the web socket. As KDB+ supports only asynchronous web sockets for now, I store a negative of that handle in the global .admin.wsh. I immediately use that handle to send a grid filled with ones to the browser (converted to a string by the .admin.bToString function), just to see some action on the connection event.
Then in the function that receives state updates from the grid cells there is a line

if[.admin.wsh<0;.admin.wsh .admin.bToString .admin.states t];

which sends the current grid state to the browser as a string whenever there is someone connected. That’s pretty much all on the q side.
On the Elm side things are simple enough as well

import String
import WebSocket as Ws

main = dispGrid  Signal String -> Signal String
helper = Ws.connect "ws://localhost:17400"

dispGrid:String->Element
dispGrid s = flow down (map dispStr (String.split "," s))

dispStr:String->Element
dispStr s = flow right (map dispChar (String.toList s))

dispChar:Char->Element
dispChar c = (if c=='1' then color black else color white) (spacer 30 30)

This connects to the server at port 17400 and displays strings that are sent from it, parsing them as comma separated lines of characters “0″ and “1″. After putting this code in the life.elm file and compiling with elm --make --bundle-runtime Main.elm" I get a standalone life.html file.

If you want to play with this

all code is on GitHub.

To see the simulation start the life.admin component (see my previous post for details)

yak start life.admin

Then load the life.html file into a browser. Upon connection it should display the grid as a black square. Then start the grid cell processes:

yak start grid

For larger grids the system takes quite a long time to start and set up connections. For example for the 12 by 12 grid it takes about 2 minutes. I’m not sure what is the reason it takes so long. The first couple of generations are also rather slow – about 1/sec. However, after about 100 generations the speed improves and on my (virtual) machine I get about 70 generations per second.

Here is how the start of the simulation looks like in the browser:

LifewithEC_Elm

 

And a bonus: a one-line implementation of Conway’s Game of Life in q.

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.

Read the rest of this entry »

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.

The goals of the project are very ambitious. The ProofPeer team is planning to build a massively collaborative theorem proving system that would be able to handle millions of users, tens of thousands concurrently, while being sound, extensible and relatively simple to use. I am really trying to restrain my sometimes excessive skepticism here, but come on: millions of people doing formal proofs? Like, who is going to force them to do that? Has formalized mathematics become cool recently and I haven’t noticed?

In my opinion (at least as far as far as formalized mathematics is concerned) there are two preconditions for attracting users to such system – a readable proof language and foundations based on some sort of set theory. Let’s talk about the readability. Of course readability is a very subjective term. However, people who may want to do formal proofs have been most likely trained in mathematics. They are used to proofs that look and can be read in a very specific way. This gives a good criterion for readability: a formal proof is readable if someone familiar with standard mathematical notation can look at it and have a good guess on what assertion is proven and why the assertion is true. Now, let’s look at an example proof written in ProofSript – the ProofPeer forrmal proof language:

proof
   REPEAT all_intro_tac
   REPEAT imp_intro_tac
   conj_intro_tac
   REPEAT assumption_tac
end

This is nor readable, at least in the way I understand it.

The second condition is familiar foundations. In my opinion this is a bit less important than readable presentation of proofs, but still a foundation that is radically different from what mathematicians already know creates an additional barrier for new users. The ProofPeer site suggests that the foundation must contain HOL and should contain ZFC. The decision is to focus on one logic rather than create a generic system that is able to support many logics. The argument here is that supporting many logics would lead to fragmentation of community. I think this is a mistake. Supporting only one logic will probably lead to the situation that potential users who do not like say HOL, but prefer ZFC (like myself) will not become actual users.
Anyway, although I think chances of ProofPeer project reaching its goals are extremely small, I still think that a lot of good research may come out from it. If not exactly in formalized mathematics, then perhaps in formally verified software? As a programming language and a proof language ProofScript may become a better Coq.

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.
Read the rest of this entry »

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.

Java, Mockito and ArgumentCaptor

September 3, 2013

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.

Read the rest of this entry »

IsarMathLib 1.9.0 released

July 26, 2013

I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the isarmathlib.org site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.

Here is a short description of what is in the new theories:

Read the rest of this entry »

Gowers and Ganesalingam

May 12, 2013

There is a series of posts at the Timothy Gowers’s blog about software that can “solve mathematical problems” which he has been working on with Mohan Ganesalingam for the last three years. The word “problems” is used here in the way a mathematician would use it – it’s really about software that can support a mathematician trying to write a proof of a theorem. The goal is for the program to write proofs that look like ones produced by a human. The experiment Gowers sets up on his blog presents several theorems with proofs written by two humans (an undergraduate and a graduate student) and one created by the program and asks the readers to guess which proofs are written  by whom. The results are truly remarkable – while I, and most of the audience, could have a good guess which proof is written by the software, I believe I could guess it only because I had known one of the three proofs was such. If a student submitted such proof as homework to me, I would have no suspicion at all.

Read the rest of this entry »

IsarMathLib 1.8.0 released

February 25, 2013

I have released the 1.8.0 version of IsarMathLib. This version works with the new Isabelle2013 (released about two weeks ago). The new material in this release mostly comes from contributions by Daniel de la Concepción Sáez, who added 5 theory files with about a hundred theorems about general topology. The subjects range from convergence of nets and filters and related continuity properties of functions, through some generalized notions of compactness and connectedness, to rather abstract (like, category theory abstract) subjects of heredity and spectra of topological properties. Unfortunately, it will take some time before those theories will be presented on the FormalMath.org site, as my parser is not good enough to parse Daniel’s advanced Isar style.  I will work on this though and in the meantime an interested reader can have a look at the Isabelle generated full proof document or the outline.

As for myself, I have finished the proof that the function (x_0, x_1,...,x_{n-1})\mapsto \sum_{i=0}^{n-1}x_i is continuous in the natural topology on the space of n-element sequences of a topological group.


Follow

Get every new post delivered to your Inbox.