Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 23 Feb 1994 19:18:36 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28992; Wed, 23 Feb 1994 12:00:43 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA28988; Wed, 23 Feb 1994 12:00:38 -0700 Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk with LOCAL SMTP (PP) id <00879-0@goggins.dcs.gla.ac.uk>; Wed, 23 Feb 1994 18:57:24 +0000 Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA04495; Wed, 23 Feb 94 18:57:21 GMT From: tfm@dcs.gla.ac.uk Message-Id: <9402231857.AA04495@switha.dcs.gla.ac.uk> To: Phil Windley Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Re: Partial evaluation in ML? In-Reply-To: Your message of "Wed, 23 Feb 94 11:28:18 MST." Date: Wed, 23 Feb 94 18:57:20 +0000 > Perhaps I'm missing something obvious, but.... > > When I do the following: > > > let dist_thm_list = > let thms = CONJUNCTS Instruction_distinct in > thms @ (map GSYM thms);; > > > let INST_DIST_TAC = REWRITE_TAC dist_thm_list;; > > HOL responds with: > > INST_DIST_TAC = - : tactic > Run time: 14.9s > Garbage collection time: 31.4s > Intermediate theorems generated: 12792 > > > Notice the "Intermediate theorems generated: 12792". This implies that HOL > is doing partial evaluation on curried arguments, doesn't it? Is it > really, or is it doing something simpler which I'm missing? Yes - this is just one example of a rather common efficiency strategy in HOL. Suppose you have a curried function RULE : theorem -> (theorem -> theorem) where there is scope for RULE to do some `work' immediately when it receives the first argument. Furthermore, suppose that, for fixed th, one uses "RULE th" over and over. Then it makes sense to pre-evaluate the partial application of RULE to the first argument th, and then use the saved result of this pre-evaluation. Recognizing this, many of the built-in high-level tools are deliberately designed so that they actually *do* some computation when partially applied in this way. Try, for example, partially applying INDUCT_THEN to an induction theorem. Or, as Phil has just discovered, apply a REWRITE rule/tactic to the list of rewrites. Technically, it's not quite partial evaluation (by the way) but it's an optimization trick that I and other implementors are very fond of. Incidentally, I just happen to have embarked last year on some collaborative investigations of using *real* partial evaluation to speed up HOL. Stay tuned for the results! Tom