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: <20875.9302091013@frogland.inmos.co.uk>
Subject: Re: Basic Rules
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Tue, 9 Feb 1993 10:13:53 +0000 (GMT)
In-Reply-To: <"swan.cl.ca.414:08.02.93.19.07.43"@cl.cam.ac.uk> from "Tom Melham" at Feb 8, 93 07:07:35 pm
Content-Type: text
Content-Length: 1410

Tom Melham has said:
> schneide@de.uka.ira asks:
> > Now my question: Is there any special reason for using
> > these primitive operators and basic inference rules? And
> > if not, wouldn't it be reasonable to have a minimal set 
> > of basic rules? And if there are reasons for efficiency,
> > why don't we take REWRITE_RULE as a basic rule of inference,
> > since this rule is used very often.
> 
> I think part of the reason behind the particular set of inference
> rules used in the primitive basis of HOL is that the system was
> originally built on top of LCF, and it therefore inherited quite
> a bit of its logical structure from that system. 

In fact HOL already has a "minimal set" of rules as many of the derived
rules while having an official definition using basic inference are
optimised by direct coding.

For rewriting, with the optimisations of conversions I'd have thought
that actually its performance now must be reasonably close to a
"primitive" rewrite rule? Also, if you wan't to make rewriting
primitive which version(s) do you want? REWRITE_RULE, ONCE_REWRITE_RULE
etc.

--------------------------------------------------------------------------
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