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


Tom Melham writes:

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

Well, there need be no "subsequent search" for beta-redexes; one can generate
the appropriate depth conversion as part of the matching procedure. A selection
of possible reductions can be precomputed from the rewrite rule before the
target term is seen, and whittled down quite efficiently later during matching.
(There are a few tricky issues about exactly which beta-conversions the user
*wants*, but let's leave that aside.)

Certainly the matter of actually doing the depth conversions is unavoidable.
However I believe that it is almost as efficient as a handcoded alternative
which works in the same way (perhaps with partial evaluation it would be
identical?) Of course it may be that an alternative inference pattern is
quicker than higher order instantiation of a proforma (this is the case for
some of the existing quantifier conversions which are mostly very efficient),
but in my opinion the margin is small, and outweighed by the gain in elegance
and regularity.

John.