Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
To: hol2000@leopard.cs.byu.edu
Subject: Re: What's up for grabs?
In-Reply-To: Your message of "Thu, 26 May 94 09:25:27 EDT." <9405261325.AA13296@msiadmin.cit.cornell.edu>
Date: Thu, 26 May 94 21:22:50 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:105240:940526202303"@cl.cam.ac.uk>


Garrel writes:

| I have a bunch of ideas that might be relevant to putting together HOL2000.
| But it's not clear to me which of my ideas really are relevant, because I'm
| not sure what kinds of changes the following statement from the hol2000
| announcement rules out:

I think *nothing* should be ruled out, as a topic of discussion at least.

HOL has been applied in a wide variety of areas. The general philosophy has
been to keep using it despite its shortcomings, and so come to appreciate more
deeply what those shortcomings are (and perhaps appreciate that some of them
are not shortcomings at all). To quote Kreisel's slogan "ENOD: Experience, Not
Only Doctrine". A critical analysis of HOL can be split quite cleanly into
logical issues and implementation issues, although of course these can interact
in a complex way and it's not clear where some things (e.g. abstract theories)
belong.

The HOL logic is extremely simple. However some features make it inflexible,
most especially the lack of dependent types. We can try modest extensions to
the logic which have considerable potential, e.g. Tom Melham's type
quantification. On the other hand, we can use a much more complex type theory.
However some may say that almost no type theory more complex than HOL's can be
said to be as conceptually simple (let alone familiar to mathematicians) as set
theory. So might one take set theory as basic and use type theory as an
organizational tool built on top of that (or not at all)?

The HOL approach is to reduce everything at runtime to very simple rules of
inference, and to make all theories definitional extensions of the base logic.
This offers undeniable advantages of coherence, security and extensibility,
but it can lead to inferior performance and make derived rules quite hard to
write. A reasonable starting point for the discussion might be to gather
experience of attempting to write complex decision procedures as HOL derived
rules and decide whether:

 1 The procedure is almost as efficient as it would be when written by more
   ad hoc means. For example, rewriting almost certainly falls into this
   category, as lookup in discrimination nets dominates (I soon hope to do
   significant work profiling HOL to find if this kind of guess is true).

 2 The procedure is dramatically more inefficient when implemented as a
   derived rule. Probably BDDs fall into this category, though I will be
   reporting work along these lines at the HOL meeting in Malta which may make
   the situation appear less than hopeless.

In the second case one can then ask: is that procedure sufficiently important
in typical applications to justify some basic changes in the system to
accommodate it? If so what are those changes? Would just introducing
generalized abstractions be enough, or do we need a different logic, or
computational reflection, or what? Are all such palliatives hopless and must we
simply rely on an external tool?

If we reach this last conclusion, how are we to regulate the use of external
tools? Ralf Reetz suggested a slow and fast mode, an idea which has often been
mooted before. Certainly it would be trivial to add tags to the theorem data
structure to say "this relies on a BDD package" or "this relies on a computer
algebra system", and have these propagate appropriately through inference
rules. A much more complex idea, but one which automatically combines the use
of slow and fast modes, is Richard Boulton's scheme of "lazy theorems".

In all these decisions there can arise a tension between theoretical elegance
and efficiency or ease of use. Perhaps the HOL philosophy in the wider sense is
to give more weight than usual to the former, and find more often than not that
the expected tension is not there after all.

John.