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; Tue, 26 Sep 1995 17:43:26 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA066281516; Tue, 26 Sep 1995 10:05:16 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA066111463; Tue, 26 Sep 1995 10:04:23 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 26 Sep 1995 16:34:47 +0100 X-Uri: To: Konrad Slind Cc: John.Harrison@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu Subject: Re: At a Los for something to do? (III) In-Reply-To: Your message of "Tue, 26 Sep 1995 14:51:02 BST." <95Sep26.145108met.8084@sunbroy14.informatik.tu-muenchen.de> Date: Tue, 26 Sep 1995 16:34:42 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:282230:950926153501"@cl.cam.ac.uk> As you know, I favour implementing the quantifier movement conversions as rewrite rules, using basic second order matching. Given that, most of these "prenexing" operations can be implemented by a set of rewrites, so one could have say, PNF, NNF, DNF, CNF and other conjunctions of rewrites. But in some cases, the default rewriting strategy might be highly inefficient, or even wrong, and implementing these normalization strategies efficiently is surprisingly subtle. So perhaps there is a justification for custom conversions of the sort you describe. For example, rewriting with associativity theorems becomes amazingly slow on big terms, so I once wrote a special conversion (30 or so lines long!) for right-associating terms. John.