Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <3547.9501061102@frogland.inmos.co.uk>
Subject: Re: Difficulties with large terms
To: John.Harrison@cl.cam.ac.uk (John Harrison)
Date: Fri, 6 Jan 1995 11:02:07 +0000 (GMT)
Cc: info-hol@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:198010:950105221016"@cl.cam.ac.uk> from "John Harrison" at Jan 5, 95 10:10:07 pm
Content-Type: text
Content-Length: 3632

John Harrison has said:
> In my recent work on BDDs, I've been playing with some rather large terms,
> and I've noticed an unpleasant bottleneck.

... HOL seems to have several things which turn out to be quadratic (or worse)
but only get noticed on very big terms!

> Part of the appeal of the LCF/HOL approach (and a good answer to the
> assertion that decomposition to primitive inferences is fundamentally
> inefficient) is that transformations from |- E[t] to |- E'[t] can be done
> by appealing to a pre-proved theorem, rather than repeating a perhaps
> difficult proof every time. That is, if we store the theorem:
> 
>   |- !x. E[x] ==> E'[x]
> 
> it may then be instantiated as required:
> 
>   |- E[t] ==> E'[t]
> 
> and we may then perform a Modus Ponens step with |- E[t] to get |- E'[t].
> 
> All very well, but the Modus Ponens step performs an *alpha-equivalence*
> test between E[t] and E[t]. This of course returns "true", but necessitates
> a complete traversal of E[t]. If |t| is large, this is very inefficient. If
> MP tested for *equality* instead, however, then then test would (in a
> decent compiler) short-circuit with a pointer EQ when it reaches |t| in its
> traversal. Thus the complexity would be the same as any purely applicative
> implementation of such a transformation.
> 
> So, I believe that HOL primitives such as MP and TRANS should allow quick
> pointer EQ tests, otherwise things like this are going to be difficult.
> Some possibilities are:
> 
> * Put an EQ test in the "aconv" code (but does ML make such a thing
>   available? I don't think so...)
> 
> * Change all primitive rules to use "=" rather than "aconv" (arguably a
>   retrograde step from the usability point of view; one would want to build
>   "aconv" versions on top).
> 
> * Change all primitive rules to use "t1 = t2 or aconv t1 t2" instead of
>   "aconv t1 t2". A bit ugly but reasonable. The only problem is that
>   failures are going to take twice as long. But does one ever expect
>   failures? Not so often I think.

The problem with using equality is that (if its permitted) it will perform
a traversal down the trees to see if they are equal - if this goes in
aconv then it could make aconv quadratic!

Also, in HOL90, since it uses de Bruijn style indexes for lambda variables
then eq and aconv have the same complexity - except for the probably
short circuit in equality where two identical values (i.e. same memory
object) are compared.

What you really want is a test for "identical" objects in aconv to
do the same short circuiting. Unfortunately, I don't think this is
a facility available in SML, but looking into the SMLofNJ code it
seems that the polymorphic equality definition uses the function
Inline.ieql however this seems fairly well hidden from the toplevel
of SML! An SMLofNJ expert might know how to excavate this - however
this would make the code SMLofNJ specific.

Basically, what is need is not an exact "=" function but a "fast
approximation" which only returns true if the terms are equal but may
return false negatives if it can't quickly determine equality.


--------------------------------------------------------------------------
david shepherd:                           sgs-thomson microelectronics ltd 
email:des@inmos.co.uk                                      1000 aztec west
tel: 01454-616616 x 638                                        almondsbury
www: http://www.inmos.co.uk/~des/welcome.html                      bristol
                                                                  bs12 4sq
"whatever you don't want, you don't want negative advertising"          uk