Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: chou@CS.UCLA.EDU's message of Tue, 12 Jan 1993 09:34:53 +0100 <9301120834.AA10014@maui.cs.ucla.edu>
Subject: BETA_CONV
Message-Id: <93Jan13.000602met.8121@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 13 Jan 1993 00:05:52 +0100

Ching Tsun asks

> What is the time complexity of HOL90's BETA_CONV's renaming algorithm?
> O(n) or O(n^2), where n is the size of the term being renamed?

This is a good question. At one time, when I had a pure DeBruijn subst,
there was no renaming, hence no renaming complexity. (The complexity had
shifted to dest_abs, if you can believe that.) The problem with a pure
DeBruijn solution, as Elsa pointed out to me, was that it interacted
badly with "snarfing". For example let tm = (--`\y.x y`--). In a dB
representation, bound and free variables are in separate syntax classes,
so tm might be represented by something like (ignoring types and
assuming hol90ish term representation)

    Abs{Bvar = "y", Body = Comb{Rator = Fv "x", Rand = Bv 0}}

Then 

    subst [{redex = `x`, residue = `y`}] tm

would give the representation

    Abs{Bvar = "y", Body = Comb{Rator = Fv "y", Rand = Bv 0}}

Unfortunately, this would print out as

    \y. y y

and one wouldn't be able to pick the prettyprinted term with the mouse
and re-parse it into its original representation. This is bad news if
you are trying to grab a term off the assumption list in the goal stack
to feed to a tactic, for example.

(This is one, seemingly minor, difference in the requirements on lambda
terms in our theorem prover and a functional language: prettyprinted
terms must, as often as possible, be reparsable to themselves. Of course
the other major difference is that functional languages don't have free
variables.)

Anyway, to get back to the story: I kept the dB representation, but
renamed bound vars when a term would otherwise not be reparsable, i.e.,
when free vars in the incoming term would be captures by the scope,
i.e., the standard requirement. The cost is probably O(n^2), because of
re-traversal of the term from the binding occurrence that gets renamed,
but I know a solution that is O(n); I just haven't implemented it, since
among the many critical things confronting me, it doesn't seem to be the
most critical. In my opinion, and I'm totally off topic here (and
perhaps flagrantly wrong!), the bottleneck in the HOL system these days
is not the system; it's the user and the low level at which they
operate. Take the library of sets for example: it takes hol90 approx. 45
seconds to prove all the theorems in the library. How long did it take
to write the proofs?

In general though, the efficient representation of the lambda calculus for
theorem provers and functional languages is still a research topic.


Cheers,
Konrad.