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: <3411.9301131443@frogland.inmos.co.uk>
Subject: Re: Bottleneck in HOL (was Re: BETA_CONV)
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Wed, 13 Jan 1993 14:42:59 +0000 (GMT)
In-Reply-To: <13254.9301131405@godel.dcs.ed.ac.uk> from "Mike Fourman" at Jan 13, 93 02:05:35 pm
Content-Type: text
Content-Length: 2505

Mike Fourman has said:
> David Shepherd <des@uk.co.inmos> 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!). 

> We also realise that designers are willing to rely on many informal tools,
> They will not use formal methods if they cannot be integrated with these
> informal tools. The next release of LAMBDA will include a system of 
> tagging results that depend on external tools (for example, model
> checkers, simulators, or direct user input). This will allow users to
> appeal to (supposedly reliable) oracles, but will ensure that any
> consequences are appropriately annotated.

This sounds similar to Mike Gordon's message about a "TOOL" assumption
and my follow-up - however having this annotation outside the formal
language is probably best rather than trying to encode a representation
of it in the logic. Effectively with the annotations I assume you can consider
a theorem (or rule?) to have both logical assumptions (the assumptions to
the theorem) and meta-assumptions (the tool annotations) which state what
the packages the theorem depends on. These are different levels of
concepts so seperating them seems preferable.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                New Year Resolution for 1993: Start using capital letters.