Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <2981.9301131050@frogland.inmos.co.uk>
Subject: Re: Bottleneck in HOL (was Re: BETA_CONV)
To: Richard.Boulton@uk.ac.cam.cl (Richard Boulton)
Date: Wed, 13 Jan 1993 10:50:49 +0000 (GMT)
Cc: slind@de.tu-muenchen.informatik, info-hol@edu.uidaho.cs.ted
In-Reply-To: <"swan.cl.ca.363:13.01.93.09.48.08"@cl.cam.ac.uk> from "Richard Boulton" at Jan 13, 93 09:47:58 am
Content-Type: text
Content-Length: 4142

Richard Boulton has said:
> 
> Konrad writes:
> 
> > In my opinion, and I'm totally off topic here (and
> > perhaps flagrantly wrong!), the bottleneck in the HOL system these days
> > is not the system; it's the user and the low level at which they
> > operate. Take the library of sets for example: it takes hol90 approx. 45
> > seconds to prove all the theorems in the library. How long did it take
> > to write the proofs?
> 
> I don't disagree with this. However, one way to get the user working at a
> higher level is to provide more decision procedures and `intelligent' tactics.
> These can be very computationally intensive in any system, but especially in
> HOL. If you give the user a tactic that takes a decade to run they simply
> won't use it, but will look for a slick manual proof instead. So, we're back
> to making HOL `more efficient', whatever that means.

However, from a perspective of trying to move proof techniques into 
"real world" design use it is vital that the users have
(semi-)automated proof methods. If in a design which a designer would
see as being  trivial (and compared with state of the art design I
think most designers would consider much that has been proved with HOL
as being fairly trivial) design steps are taking hours to complete by
an automated proof then they are going to take a lot of convinving that
it is a good thing. If you tell them that they need to find a "slick
proof" instead then that too is no good as they probably have neither
the time nor the inclination to do this.

I think it is great that HOL is (or could be !) a very clean
implementation with everything going back to the 8 primitive rules, 5
axioms and 2 definition methods. This gives a good clean base for
investigating further developments etc. However, for use in an
industrial environment I think that pragmatic decisions need to be
taken so that certain well chosen areas are done directly, rather than
by primitive inference. For example, while it is good that you can
prove |- (23 * 17) = 391 by Peano arithmetic, I would be quite prepared
to believe that this could be evaluated correctly in an ML evaluation
function in much less time than 21s! From seeing a demo of ICL HOL (aka
ProofPower :-) calculate factorial 10 virtually instantaneously I think
that this is the sort of pragmatic view they have taken.

Similarily I have recently come across significant problems when trying
to automate a style of design "synthesis" in HOL. The techniques tend
to generate a large quantity of existentially quantified variables
(o(100)) which need to be moved around a bit and then pruned. The
problem is that when doing something to a long list of existential
quantifiers each has to be handled seperately and  each of these
usually requires finding the free variables of the body. The result is
that the free variable evaluation is performed 100 times where a
carefully coded, but "dirty", version would only do this once. The
result is that I have various (simple) design transformations which
take 5 to 10 minutes to do in HOL - I've seen a recent demo of Abstract
Hardware's Lambda/DIALOG system which does similar  things virtually
instantaneously.

I'm not suggesting that people should blithely write special purpose
routines at will using mk_thm, because that is a road to disaster.
However, it must be appropriate when moving proof tools into use in
particular domains to recode efficient versions of "standard" proof
procedures.

Perhaps with a HOL written in SML (such as ICL HOL or hol90) it is
possible to use the module structure of SML to flag (and limit) the use
of such steps outside the core system (i.e. by seeing if a module needs
to import mk_thm you know whether it may be insecure and thus needs a
better check). Also, for pedants, you could always provide a clean
version of the same module.


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                New Year Resolution for 1993: Start using capital letters.