Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: john.harrison@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
Subject: Re: Difficulties with large terms
Message-Id: <95Jan26.150403met.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 26 Jan 1995 15:03:58 +0100


> As you can see, Inf(1) is linear in the number of nodes, whereas
> Inf(2) is quadratic. Maybe with enough ingenuity one can do better
> without changing the primitive rules, but as I said originally, there
> are some quite general arguments in favour of putting an equality test
> in there.

I interpret this evidence as supporting a change to aconv, *not* for
changing the implementation of inference rules. A change to aconv so
that it quickly said "true" when presented with identical terms would
benefit all inference rules, not just TRANS and EQ_MP. To do this
properly would involve a complexification of the representation of
terms.

I think there are 2 interesting research areas highlighted by John's
investigation:

1. HOL doesn't have a particularly efficient implementation of the
   lambda calculus. I don't think anybody else does either - it's a
   major problem to have optimal implementations of substitution, aconv,
   computation of free variables, computation of types, and
   con-and-de-struction of terms. 

2. When one is working in a restricted logical setting, such as BDDs,
   certain algorithmic and representational optimizations are valid in
   the kernel of the theorem prover, e.g., replacing aconv with EQUAL
   and perhaps even EQUAL with EQ (if ML had EQ!). As yet we have no
   mechanism for doing this sort of data/algorithmic refinement of the
   abstract datatype of terms. Reflection and partial evaluation are two
   mechanisms that have been suggested but they haven't had much success
   that I know of.

Konrad.