My research and investigations

Archive for February, 2011

A Web Interface for HOL

HOL output has a lot of math symbols, which are encoded in Unicode. Displaying these math symbols in DOS when running HOL in Windows is not satisfying. To solve this problem, I developed a simple Java server that talks to HOL in the background, and I can use the web-browser to talk to the server. With such a system I can easily get the math symbols in the browser, and also enhance the display of HOL input/output with colors.

The code for my little work is in

This is also my first experience with Bitbucket, a free source code hosting based on Mercurial, a distributed version control system. There is a nice short tutorial by Joel Spolsky, which explains clearly and simply how to use Mercurial.


Running Linux in Windows

With VirtualBox, it’s pretty easy to run another operating system as long as you have a modern PC: plenty of memory, plenty of hard disk space.

However, it is still a great pleasure to see that this really works. VirtualBox uses hardware virtualization, making it a Hypervisor. Hence it is able to simulate the entire operating system, down to the connecting devices.

I’ve installed Virtual Box 4.0, and run a VM based on Ubuntu 10.10. I worked with Unix terminals long time ago, so this “Desktop Linux” is a new experience for me. Such is the advance of technology.

As a Java developer, I like the way that Java is already included in Linux. There is also the GCC compiler, so there’s a lot of programming tools I can work with.

Both VirtualBox and Ubuntu comes with heaps of features. These new toys will keep me busy for weeks!

Interactive Theorem Proving

The HOL System Tutorial is a fairly gentle introduction to using the system HOL. It provides screenshots from the interactive sessions, so you can follow what’s happening even if you don’t have the system installed. Better still, download and install HOL, then follow the tutorial to verify the sessions and get a hands-on experience with the system.

The first substantial example is a proof of this theorem: that there are infinitely many primes. The classic proof by Euclid is considered as a proof from “The Book” — in which God keeps the most elegant proof of each mathematical theorem, according to the mathematician Paul Erdös. During a lecture in 1985, Erdös said, “You don’t have to believe in God, but you should believe in The Book.”

However, to rephrase this proof in HOL, many basic concepts needs to be established first: what is a prime? how to define divisibility? All these boil down to logical statements about natural numbers.

The actual proof process in HOL is assisted by the Proof Manager. There are actions to put a goal to the manager, expand the goal by tactics, which are strategies to pick either known facts or lemma from a HOL theory. The expansion of a goal usually gives subgoals, which can be further expanded until everything is known, upon which the initial goal is proved. Of course, picking the correct strategies take some understanding and experience. The Proof Manager allows you to advance a step, backup a step, or redo from the start. All these techniques are demonstrated in this example of the Tutorial.

In the end, Euclid’s proof of the infinity of primes is done in about 10 lines of HOL code, after much polishing. This is finale of a whole chapter with more than 30 pages!

ML as a Functional Language

The challenge for any programming language X which claims to be general-purpose is this: can X compile itself? More specifically, can language X be used to write a compiler that compiles itself?

Most functional languages can perform this trick: John McCarthy’s Lisp in Lisp is a classic. Nowadays, there are Scheme in Scheme compilers.

Therefore it is no surprise to find an ML compiler in ML, specifically an SML compiler in SML. This is the mission for MLKit, even from version 1 in 1993. The project was to put the Definition of Standard ML (1990) into an actual implementation in SML. Since then, the 1990 Definition has been revised, and MLKit has evolved into version 4 with better and better compilation and implementation. This is a nice example of the expressive power of ML.

At first, the goal of MLKit was to understand the ML language itself. Both compilation and implementation are coded with clarity, rather than efficiency. However, this understanding provide the basis of other efficient ML implementations, including Moscow ML and Caml.