[MLton] Implementing HOL in MLton - ideas wanted

[Michael Norrish]

HOL (http://hol.sf.net) is a theorem-proving system supporting the
modular development of logical theories.  Currently, we use Moscow ML
as our implementation language.  This has two problems:

  1. Moscow ML is quite slow.  In some applications we'd like to take
     advantage of what we imagine will be the superior performance
     available from other systems.
  2. Moscow ML's development seems to have stalled.  The current
     release supports an older version the Basic Library, and there's
     no hint that a new release is on its way.

On the other hand, Moscow ML has let us implement a system that
supports multiple modes of use with gratifying flexibility.

Rather than presuppose a particular implementation scheme, I'd like to
describe the situation from the perspective of what we think we need,
and then invite comments on how we might be able to use MLton.

A.   First off, HOL is based on a smallish kernel of ML code.  Any HOL
     execution will involve this code, which defines the type of
     theorem, and the primitive rules of inference.

     Users can manipulate and combine theorems to create new theorems,
     thereby performing proof.

B.   Theories are the next ingredient: when a user proves some set of
     theorems (literally, creates a particular set pf values of type
     "thm"), they want to make their work persistent so that these
     theorems can be built on in future sessions.  Such a set of
     theorems (including the definition of new constants, and the
     proof of facts about them) is what we call a "theory".  In future
     sessions, users must be able to use these theories, and
     preferably without this use requiring time-consuming proofs to be
     repeated.

C.   The next bit is where it gets complicated: theories can be
     accompanied by code.  For example, once you have a theory of the
     natural numbers, you'd like to be able to prove linear formulas
     automatically.  There is SML code for doing this, but it only
     makes sense in the context of the HOL theory of natural numbers.
     This dependency is made concrete by the fact that the SML code
     refers to and uses theorem values from that theory.  (Recall:
     theorems are ML values, manipulated by our kernel from A above,
     but may have been created in a previous session, and recovered
     through our persistence mechanism B.)

     This happens in the distribution of HOL (i.e., we distribute
     decision procedures to accompany various theories), but we'd also
     like it to be easy for users to do themselves.

                    ------------------------------

I won't describe our existing Moscow ML implementation at this stage
because it might queer the pitch, but I will describe how the Isabelle
system achieves the above.  I'm happy to do this becaue I'm confident
any MLton solution wouldn't look like it, and because I think it is
aesthetically awful, and wouldn't consider it anyway. :-)

Isabelle has the same sort of ML kernel as HOL.  Its solution to
problems B and C is to use an implementation's top-level interactive
loop (SML/NJ and PolyML are supported).  There fresh code can be
loaded with 'use'.  So, when a context supporting your linear
arithmetic procedure is established, you can just 'use' the
procedure's code, and you're in business.  Persistence is achieved by
dumping heaps at the end of interactive sessions, and reloading them
when a new session begins.  (Moscow ML can't export and reload heaps,
so doesn't work with Isabelle.)

My big objection to this approach is that it requires a separate heap
for all possible combinations of logical/code entities.  There are
also difficulties with the creation of custom standalone executables
that perform automatic logical analyses (a combination of the kernel's
operations with a custom decision procedure for example).

I can describe our current Moscow ML solution to this problem, as well
as our much older SML/NJ implementation in another post if people need
further prodding. :-)

Regards,
Michael.