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
Subject: Re: "Meta" rewriting
In-Reply-To: Your message of "Mon, 11 Jul 94 11:30:57 PDT." <9407111831.AA20162@maui.cs.ucla.edu>
Date: Sat, 16 Jul 94 16:38:46 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:205550:940716153853"@cl.cam.ac.uk>


I have an experimental implementation of limited second order matching,
which I use to implement the quantifier conversions by simply throwing in
theorems as rewrites. I feel strongly that this is the right way to go.
It's very wasteful to have ad-hoc conversions for such instances, and
very tedious to perform explicit instantiations in the cases where there
aren't any. Furthermore, it's a bit tiresome to alternately rewrite and
call conversions like BETA_CONV in proofs (I think old LCF had a facility
for throwing conversions into the rewriting tactics). Much easier just to
perform a big rewrite.

The ideal, it seems to me, is to use such matching throughout the system
by default (at present I control it via a global flag). Of course there
are a few sticky problems, like controlling bound variable names rather
than inheriting those of the rewrite rule (Ching Tsun remarked on this),
and deciding just how general to make second order matching. But it's
*very* convenient to have something. Most conversions can be expressed as
second order rewrite rules. Even beta-conversion can:

 |- !P. (\x. P x) y = P y

although eta-conversion presents a slight pitfall, since a higher order
rewrite with:

 |- !P. (\x. P x) = P

is apt to go into an infinite loop at every abstraction term.

Tom Melham 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
rewriting workhorse it is important that the term nets code be modified
to allow higher order rewrites. I have written a very simple new
implementation, but it needs careful profiling to judge how its
performance compares. (Apart from the issue of higher order rewrites,
there are many useful-looking changes that could be made to term nets.)

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

John.