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: <9407201740.AA19079@switha.dcs.gla.ac.uk>
To: John Harrison <John.Harrison@cl.cam.ac.uk>
Cc: info-hol@leopard.cs.byu.edu, terra@diku.dk, tfm@dcs.gla.ac.uk
Subject: Re: "Meta" rewriting
In-Reply-To: Your message of "Wed, 20 Jul 94 15:38:42 BST." <"swan.cl.cam.:005190:940720143915"@cl.cam.ac.uk>
Date: Wed, 20 Jul 94 18:40:12 +0100

John Harrison opines:

>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

I agree that such an approach is certainly possible. My main point was
that the programming couldn't be quite as naive as one might at first
imagine - as this discussion illustrates.  Indeed, pre-computation of the
depth conversion is precisely what the cited example (INDUCT_THEN) does.
An interesting twist is that I found the computed depth conversion gave
the best performance when I built into it some "knowledge" of the
structure of the terms that were to be expected (e.g. "a conjunction of
base cases and step cases, the latter being implications, etc...").  This
too, of course, might be attempted automatically.

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

Not only that, but if we supply a sufficently powerful infrastructure in
the form of good utilities, this will make it easy for novice users to
create efficient tools themselves.

Perhaps we should have a pub-meeting on these ideas in Malta...

Tom