Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9407191443.AA17059@switha.dcs.gla.ac.uk>
To: John Harrison <John.Harrison@cl.cam.ac.uk>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk, terra@diku.dk
Subject: Re: "Meta" rewriting
In-Reply-To: Your message of "Sat, 16 Jul 94 16:38:46 BST." <"swan.cl.cam.:205550:940716153853"@cl.cam.ac.uk>
Date: Tue, 19 Jul 94 15:43:45 +0100

John Harrison writes:

> | The only problem I see is that of efficiency: I'm not convinced that
> | an INDUCT_THEN, say, based on a general 2nd order matching algorithm
> | could equal the speed of the hand-coded one.
> 
> I think a rather restricted matching is adequate for most situations, and
> such matching is not much less efficient than first order matching.
> Slowness of INDUCT_THEN is seldom critical. More worrying is slowness of
> rewriting. For higher order rewriting to be acceptable as the main...

It's not really the matching part whose efficiency I'm worried about - 
mere computation of the match is of little consequence.  What concerns me
is the subsequent (1) search for places to do beta-reduction, and (2) 
depth conversion needed to effect reduction at these places.  Of course,
INDUCT_THEN doesn't really *need* to be fast; I'm just giving it as an 
example of a hand-coded special case that uses trivial second-order 
matching (just match "!n. P n" to "!n. P[n]")  followed by potentially
quite a bit of (search for) beta-reduction.  Perhaps we should follow
Isabelle, in which (I believe) all terms are internally represented
in fully beta-reduced form (logically justified, presumably, by an implicit 
inference rule or beta-axiom).

> Finally, partial evaluation of functions based on second order rewriting
> might be interesting to try. Perhaps it would improve efficiency a lot.

I agree. Something along these lines is what I already do to make INDUCT_THEN
fast (except not Partial Evaluation per se, but a similar semantic
optimization - vide my info-hol message of 23 Feb 94).  But I find the
prospect of using partial evaluation methods to *automatically* speed up HOL
code quite exciting.  See Morten Welinder's paper

   Towards Efficient Conversions by use of Partial Evaluation

at the Malta workshop for some preliminary work in the area.

Tom