Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <24071-0@swan.cl.cam.ac.uk>; Mon, 9 Mar 1992 21:51:12 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26057; Mon, 9 Mar 92 11:09:35 -0800 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 AA23601; Mon, 9 Mar 92 11:06:01 -0800 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <22036-0@swan.cl.cam.ac.uk>; Mon, 9 Mar 1992 19:06:50 +0000 To: hoove@com.oracorp Cc: info-hol@edu.uidaho.cs.ted Subject: Re: rewriting in HOL In-Reply-To: Your message of Mon, 09 Mar 92 10:40:40 -0500. <9203091540.AA02252@antiphos.oracorp.com> Date: Mon, 09 Mar 92 19:06:35 +0000 From: John.Harrison@uk.ac.cam.cl Message-Id: <"swan.cl.ca.054:09.02.92.19.07.09"@cl.cam.ac.uk> Doug Hoover asks: > 2. Has anyone collected reasonably general, but terminating collections > of rewrite rules for natural numbers, integers, other algebraic > structures. I'm not sure how general you mean - Version 2.0 of HOL includes a library "reduce" which simplifies "constant expressions", e.g. #REDUCE_CONV "(2 * 15) - (3 + (7 DIV 2))";; |- (2 * 15) - (3 + (7 DIV 2)) = 24 Run time: 1.7s Garbage collection time: 0.8s Intermediate theorems generated: 253 (As you may note from the number of intermediate theorems, the conversion really works by proof and doesn't cheat.) Owing to the way natural numbers are implemented, this cannot be implemented conveniently as a set of rewrite rules. Something I have investigated is making numerals a prettyprinting for underlying terms using a binary representation (e.g. 3 == num_of [T; T]). This makes several arithmetic operators into simple list recursions, but even then problems of leading zeros make it hard to use a set of rewrites. There are two advantages of this binary representation: * Direct manipulation of large numbers can be done efficiently * The infinite axiom schema "num_CONV" would become a proper derived rule. Against that, it would be slower on small numbers, and would have to be retrofitted to the basic num theory, because quite a lot of stuff about numbers is needed just to get to the point of being able to make list recursive definitions. More general arithmetic decision procedures are being worked on, and might appear in HOL 2.1. I give below a message from a couple of months back. John. * > Second, have people written decision/proof procedures for Presburger * > (sp?) arithmetic, or the theory of <=, or the theory of =, with only * > universal quantifiers? The Penelope and Eves provers have such things, * > and people here have found them very useful. Is something like them * > available for HOL88 and/or HOL90? * * I have been developing a proof procedure for non-existential Presburger * arithmetic (formulae constructed from numeric constants, numeric variables, * +, multiplication by constants, <=, <, =, >, >= and first order logical * connectives, which when placed in prenex normal form do not contain * existential quantifiers). My procedure is for natural number arithmetic, * but should be straightforward to port to integers, rationals and reals. The * procedure is not complete for naturals or integers but handles most * examples you're likely to want in practice. Subtraction is a problem in * natural number arithmetic. I haven't handled this yet but hope to. * * Unfortunately this is just an appetizer (sp?). The procedure is not ready * to be released yet. It *might* be ready for the next release of HOL. I am * developing it for HOL88, but it should become available for HOL90 as well. * * Richard Boulton (rjb@cl.cam.ac.uk)