Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Fri, 20 Nov 1992 12:24:10 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03009; Fri, 20 Nov 92 04:05:41 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA03002; Fri, 20 Nov 92 04:05:23 -0800 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Fri, 20 Nov 1992 12:04:21 +0000 To: austel@edu.ucla.cs (Vernon Austel) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: estimating run-time In-Reply-To: Your message of Thu, 19 Nov 92 10:00:55 -0800. <9211191800.AA25577@maui.cs.ucla.edu> Date: Fri, 20 Nov 92 12:04:15 +0000 From: Richard Boulton Message-Id: <"nene.cl.ca.471:20.11.92.12.04.22"@cl.cam.ac.uk> > The HOL timer reports the number of ``intermediate theorems generated'' - > which seems to mean the number of times mk_thm is called. Correct. > Since it is a *timer*, is this value (or was it at some point in the past) > relevent for *timing*? In scientific program one commonly uses the > the number of floating-point or vector operations to estimate run-time; > does mk_thm play a similar role for HOL? Although I have no good scientific reasons for it, the number of intermediate theorems is, for proof procedures, a good indication of the run time. For example the Sun3 I use does about 100 intermediate theorems per second. Obviously this breaks down if the program being executed does not do proof, but in many tests I have found the results to be surprisingly consistent. Even without the timing aspect, the number of mk_thm's is of interest to me, as I'm engaged in trying to reduce the number. This is for performance reasons, but the point is that even without a consistent correlation between the number of intermediate theorems and the run time, the former is significant as well as the latter. Sometimes an optimisation strategy may result in a decrease in number of mk_thm's but an increase in run time due to the overhead involved in the strategy. Richard.