Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Rob Arthan <rda@uk.co.icl.win>
Date: Mon, 18 Jan 93 10:11:27 GMT
Message-Id: <9301181011.1550.0@win.icl.co.uk>
To: des@uk.co.inmos
Subject: Re: Bottleneck in HOL (was Re: BETA_CONV)
Cc: info-hol@edu.uidaho.cs.ted


David Shepherd writer:

>	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.

Thanks for the kind words about ProofPower! In fact in many ways, ProofPower
is ``cleaner'' than the Classic HOL implementation, e.g. it has no `mk_thm',
i.e., all inference is done via valid rules (if we've implemented them
right). As in the implementation of Classic HOL, you find that the
performance you get just using the 8 primitive rules is inadequate, and
you need to implement additional rules, which are derivable, as if they
were primitive. We found, by experimenting with an earlier prototype, that
quite a small set of such `built-in' rules sufficed to give performance
at least as good as what we were accustomed to with Classic HOL (the
built-in rules we use are basically the quantifier introduction and elimination
rules and one or two rules about equality (transitivity etc.)). 

The faster arithmetic performance was a conscious design decision. It
was always clear, for example, that to prove `20,000,000 > 10,000,000'
on the basis of the Peano axioms alone must take of the order of
10,000,000 steps. To get around this, we have one further built-in
rule called plus_conv which proves theorems of the form |- M + N = K
wher M, N and K are numeric literals. Conversions are provided
for multiplication, division etc., implemented as `clean' derived rules
in terms of plus_conv, and the computation of 10! that David has seen is
done using these.


Rob Arthan. (rda@win.icl.co.uk)			ICL Secure Systems,
						Eskdale Rd.	
						Winnersh,	
						Wokingham	
						Berks. RG11 5TT