Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Fri, 16 Apr 93 12:45:43 EDT
From: shb@com.oracorp
Message-Id: <9304161645.AA13795@sparta.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Rewriting speed

How much speed increase, if any, does one get by using exactly the
right sequence of ONCE_PURE_REWRITE_TAC rewrites instead of using
REWRITE_TAC with a list of equational theorems that includes all the
ones that will be needed to produce the final result?

I've got a bunch of predicates effectively defined by structural
induction on a concrete-recursive type, and a bunch of equations that
effectively give the value of each predicate in terms of its value on
one-step-simpler and atomic members of the concrete-recursive type.
Blasting each predicate with REWRITE_TAC and all of the equations for
that predicate works, but it's slower than I'd like.  I wrote a simple
tactic to inductively figure out exactly which rewrites to apply in
doing the simplification, but I can't tell if it helped (or hurt).  It
has to repeatedly use theorem to look up theorems by name, where with
REWRITE_TAC this only needs to be done once.

So how dependent is the speed of the REWRITE_TAC algorithm on the
presence of theorems that don't apply?  The Clio prover uses hashing to
look up things it can rewrite, and if REWRITE_TAC does something
similar extra theorems might have minimal effect.  Does it?  How much
does using theorem cost?  I'm using hol90.5 if that influences the
answers.

Steve Brackin
ORA