[MLton] Implementing HOL in MLton - ideas wanted
Michael Norrish <Michael.Norrish@nicta.com.au>
Wed, 9 Mar 2005 10:19:29 +1100
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
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. :-)