Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Wed, 13 Jan 1993 16:46:07 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25846; Wed, 13 Jan 93 08:29:47 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from stroma.dcs.ed.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA25841; Wed, 13 Jan 93 08:29:12 -0800 Received: from godel.dcs.ed.ac.uk by dcs.ed.ac.uk id aa27885; 13 Jan 93 16:25 GMT Message-Id: <13901.9301131625@godel.dcs.ed.ac.uk> To: info-hol@edu.uidaho.cs.ted Subject: Re: Bottleneck in HOL (was Re: BETA_CONV) Date: Wed, 13 Jan 93 16:25:20 GMT From: Mike Fourman -------- David Shepherd replies : > Mike Fourman has said: > > David Shepherd writes > > > The result is > > > that the free variable evaluation is performed 100 times where a > > > carefully coded, but "dirty", version would only do this once. The > > > result is that I have various (simple) design transformations which > > > take 5 to 10 minutes to do in HOL - I've seen a recent demo of Abstract > > > Hardware's Lambda/DIALOG system which does similar things virtually > > > instantaneously. > > > > I'm glad to see that we've achieved something :-) However, I must point > > out that LAMBDA achieves this performance, by a carefully coded *AND > > CLEAN* proof system. The architecture of the LAMBDA proof assistant is > > influenced by ISABELLE as well as other members of the LCF/HOL family. > > This fundamental design decision provides the appropriate primitives to > > support our style of design synthesis. > > I was using the word "dirty" in the sense that it is sometimes used in > HOL to describe anything that makes direct use of mk_thm rather than > primitive inference. I'm not sure whether there's a better word to use > as naturally you want the "dirty" version to be cleanly coded (if you > see what I mean!). I think I see what *you* mean, but I believe I can't have explained clearly enough what I meant! Our synthesis does not make any use of (the LAMBDA equivalent of) mk_thm; it uses primitive inference. Our architecture supports meta-variables which you (I think) mimic using existentially quantified object-level variables. On the other hand, we do implement rewriting directly, for performance reasons (rather than reducing it to primitive inferences). Of course, this is also coded cleanly. Mike