Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <28239-0@swan.cl.cam.ac.uk>; Wed, 29 Apr 1992 09:00:02 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15562;
          Wed, 29 Apr 92 00:51:30 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA15558;
          Wed, 29 Apr 92 00:51:19 -0700
Received: from dipper.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.0) to cl id <28056-0@swan.cl.cam.ac.uk>;
          Wed, 29 Apr 1992 08:50:24 +0100
Received: by dipper.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA19177;
          Wed, 29 Apr 92 08:50:08 BST
Date: Wed, 29 Apr 92 08:50:08 BST
From: Mike.Gordon@uk.ac.cam.cl
Message-Id: <9204290750.AA19177@dipper.cl.cam.ac.uk>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: Phil Windley's message of Tue, 28 Apr 92 22:00:26 -0700 <199204290500.AA04693@panther.cs.uidaho.edu>
Subject: Historical note on conditional rewriting


The following note was prompted by Phil's last message.

LCF has conditional rewriting (implemented by Larry Paulson). When I
was modifying LCF to make HOL, I had some minor problems getting the
code to work for HOL terms rather than LCF formulae. In the rush to
finish, I postponed working on this and left the rewriting tools just
supporting unconditional rewriting. I subsequently thought up a
rationalization for not bothering to finish this job: in LCF
conditional rewriting is often used to show that terms are not UU, 
e.g. consider:

   ~(y == UU) ==> HD(CONS x y) == x

Since HOL types are sets not CPOs, it does not have to deal with this
kind of UU stuff, so (according to my work-saving rationalization)
conditional rewriting was less important for HOL and LCF and could be
experimentally omitted.

Mike