Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <10746.9301181718@frogland.inmos.co.uk>
Subject: more problems with big terms/theories
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Mon, 18 Jan 1993 17:18:51 +0000 (GMT)
Content-Type: text
Content-Length: 3227

Sometime ago there was some discussion on the length of time that HOL
takes to read in theory files. Part of this can be attributed to the
way in which HOL has to unwind all the SHARETYPES and other type
information that gets folded out of the theorems in the theory file.

I have just run into another problem where HOL explodes on big theorems
/ big terms which sheds some more light on whats going on. This may
serve as a warning for anyone expecting to want to work with very large
terms in proofs.

When theorems are stored in the theory file all unnecessary type
information is thrown away. HOL88 stores types on all nodes, though in
the theory file types are only stored on tips of the term tree. Hence
when a theorem is read in all these type nodes need to be re-instated -
this is one of the places where the time is taken. The other time is
taken in extracting nodes from the SHARETYPES structure.

I have observed two things that may cause problems:

1) Types get shared if they are sufficiently large - if so then they
get stuck in the sharetypes structure with the term type containing a
key to this element. The problem is that the type stored in sharetypes
is not itself encoded. Hence there is at best one level of
optimisation. This means that when these types get parsed back, big
type terms will not share common type structure.

2) When all the internal type nodes get rebuilt I do not think that
nodes with similar types will share the same type structures.

Both of these mean that a theory and its theorems can take up
significantly more space when stored and then reread in (in a new
theory context) than originally.

The example I have is of a theory which saves to a theory file of 2Mb
which contains 3 or 4 big definitions and a couple of theorems - as you
may gather the terms being defined are *big* with each  having an
argument which is something like a 50-tuple or a 100-tuple. When I
build this theory I get a HOL image of around 28Mb. However if I then
try to reload this theory as an ancestor in an otherwise empty new
theory the HOL image baloons to 55Mb (!) and it takes 5 minutes (+10
mins gc time :-) to load the theory.

Needless to say, this is a pretty major obstacle to what I'm doing.

Quite honestly, I can't see any easy way round this.

1) can possibly be dealt with by a sweep through sharetypes trying to
optimise subtype expressions just before the theory gets written

the only solution for 2) in my view is to drop the internal node typing
(as in hol90). Assuming all the lisp sources are "clean", i.e. if whenever
the type of a term is needed, then get-type is used (rather than cddr)
then perhaps it might be possible to provide a new routine to calculate
the type, but that looks like a major minefield.

Meanwhile, looks like I'll have to use our 64Meg SparcStation to
get my current work finished before considering the options on
where to go after hol88.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		Life doesn't imitate art, it imitates bad television
						      - Husbands and Wives